:: deftheorem defines tan SIN_COS4:def 1 :
for th being Real holds tan th = (sin th) / (cos th);