:: deftheorem defines sin SIN_COS:def 17 :
for th being Real holds sin th = sin . th;