63 Thm ("or_true",num_str @{thm or_true}), |
63 Thm ("or_true",num_str @{thm or_true}), |
64 Thm ("or_false",num_str @{thm or_false}), |
64 Thm ("or_false",num_str @{thm or_false}), |
65 Thm ("and_commute",num_str @{thm and_commute}), |
65 Thm ("and_commute",num_str @{thm and_commute}), |
66 Thm ("or_commute",num_str @{thm or_commute}), |
66 Thm ("or_commute",num_str @{thm or_commute}), |
67 |
67 |
68 Calc ("op <",eval_equ "#less_"), |
68 Calc ("Orderings.ord_class.less",eval_equ "#less_"), |
69 Calc ("op <=",eval_equ "#less_equal_"), |
69 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"), |
70 |
70 |
71 Calc ("Atools.ident",eval_ident "#ident_"), |
71 Calc ("Atools.ident",eval_ident "#ident_"), |
72 Calc ("Atools.is'_const",eval_const "#is_const_"), |
72 Calc ("Atools.is'_const",eval_const "#is_const_"), |
73 Calc ("Atools.occurs'_in",eval_occurs_in ""), |
73 Calc ("Atools.occurs'_in",eval_occurs_in ""), |
74 Calc ("Tools.matches",eval_matches "") |
74 Calc ("Tools.matches",eval_matches "") |