:: deftheorem defines LD-axioms GRZLOG_1:def 23 :
LD-axioms = GRZ-axioms \/ LD-specific-axioms;