:: deftheorem defines tan SIN_COS:def 26 :
tan = sin / cos;