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