1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Sat Jun 12 14:29:10 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Sat Jun 12 18:06:27 2021 +0200
1.3 @@ -33,17 +33,17 @@
1.4 \<^rule_eval>\<open>is_polyrat_in\<close> (eval_is_polyrat_in ""),
1.5 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
1.6 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.7 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1.8 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
1.9 - Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
1.10 - Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
1.11 - Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
1.12 - Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false})
1.13 + \<^rule_thm>\<open>not_true\<close>,
1.14 + \<^rule_thm>\<open>not_false\<close>,
1.15 + \<^rule_thm>\<open>and_true\<close>,
1.16 + \<^rule_thm>\<open>and_false\<close>,
1.17 + \<^rule_thm>\<open>or_true\<close>,
1.18 + \<^rule_thm>\<open>or_false\<close>
1.19 ];
1.20 (* ----- erls ----- *)
1.21 val LinEq_crls =
1.22 Rule_Set.append_rules "LinEq_crls" poly_crls
1.23 - [Rule.Thm ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1})
1.24 + [\<^rule_thm>\<open>real_assoc_1\<close>
1.25 (*
1.26 Don't use
1.27 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.28 @@ -54,7 +54,7 @@
1.29 (* ----- crls ----- *)
1.30 val LinEq_erls =
1.31 Rule_Set.append_rules "LinEq_erls" Poly_erls
1.32 - [Rule.Thm ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1})
1.33 + [\<^rule_thm>\<open>real_assoc_1\<close>
1.34 (*
1.35 Don't use
1.36 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.37 @@ -72,7 +72,7 @@
1.38 srls = Rule_Set.Empty,
1.39 calc = [], errpatts = [],
1.40 rules = [
1.41 - Rule.Thm ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1}),
1.42 + \<^rule_thm>\<open>real_assoc_1\<close>,
1.43 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.44 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
1.45 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.46 @@ -95,11 +95,11 @@
1.47 srls = Rule_Set.Empty,
1.48 calc = [], errpatts = [],
1.49 rules = [
1.50 - Rule.Thm("lin_isolate_add1",ThmC.numerals_to_Free @{thm lin_isolate_add1}),
1.51 + \<^rule_thm>\<open>lin_isolate_add1\<close>,
1.52 (* a+bx=0 -> bx=-a *)
1.53 - Rule.Thm("lin_isolate_add2",ThmC.numerals_to_Free @{thm lin_isolate_add2}),
1.54 + \<^rule_thm>\<open>lin_isolate_add2\<close>,
1.55 (* a+ x=0 -> x=-a *)
1.56 - Rule.Thm("lin_isolate_div",ThmC.numerals_to_Free @{thm lin_isolate_div})
1.57 + \<^rule_thm>\<open>lin_isolate_div\<close>
1.58 (* bx=c -> x=c/b *)
1.59 ],
1.60 scr = Rule.Empty_Prog});