:: deftheorem defines '=' GRZLOG_1:def 4 :
'=' = <*3*>;