:: deftheorem defines 'not' GRZLOG_1:def 2 :
'not' = <*1*>;