154 [\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
154 [\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
155 |
155 |
156 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"), |
156 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"), |
157 Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"), |
157 Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"), |
158 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
158 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
159 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}), |
159 Rule.Thm ("not_false", @{thm not_false}), |
160 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true})], |
160 Rule.Thm ("not_true", @{thm not_true})], |
161 srls = Rule_Set.Empty, calc = [], errpatts = [], |
161 srls = Rule_Set.Empty, calc = [], errpatts = [], |
162 rules = [\<^rule_thm>\<open>frac_sym_conv\<close>, |
162 rules = [\<^rule_thm>\<open>frac_sym_conv\<close>, |
163 \<^rule_thm>\<open>sqrt_sym_conv\<close>, |
163 \<^rule_thm>\<open>sqrt_sym_conv\<close>, |
164 \<^rule_thm>\<open>root_sym_conv\<close>, |
164 \<^rule_thm>\<open>root_sym_conv\<close>, |
165 \<^rule_thm_sym>\<open>real_mult_minus1\<close>, |
165 \<^rule_thm_sym>\<open>real_mult_minus1\<close>, |