:: deftheorem defines LTL0_axioms LTLAXIO5:def 5 :
LTL0_axioms = 'G' LTL_axioms;