:: deftheorem defines unit3 MOD_2:def 18 :
unit3 = 1;