:: deftheorem defines GRZ-symbols GRZLOG_1:def 6 :
GRZ-symbols = VAR \/ GRZ-ops;