1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sat Jun 12 18:06:27 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sat Jun 12 18:22:07 2021 +0200
1.3 @@ -120,7 +120,7 @@
1.4 rules = [(*for rewriting conditions in Thm's*)
1.5 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
1.6 \<^rule_thm>\<open>not_true\<close>,
1.7 - Rule.Thm ("not_false",@{thm not_false})
1.8 + \<^rule_thm>\<open>not_false\<close>
1.9 ],
1.10 scr = Rule.Empty_Prog},
1.11 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.12 @@ -179,14 +179,11 @@
1.13 \<^rule_thm>\<open>rat_mult_poly_r\<close>,
1.14 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.15
1.16 - Rule.Thm ("real_divide_divide1_mg",
1.17 - ThmC.numerals_to_Free @{thm real_divide_divide1_mg}),
1.18 + \<^rule_thm>\<open>real_divide_divide1_mg\<close>,
1.19 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.20 - Rule.Thm ("divide_divide_eq_right",
1.21 - ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
1.22 + \<^rule_thm>\<open>divide_divide_eq_right\<close>,
1.23 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.24 - Rule.Thm ("divide_divide_eq_left",
1.25 - ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
1.26 + \<^rule_thm>\<open>divide_divide_eq_left\<close>,
1.27 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.28 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.29
1.30 @@ -233,8 +230,7 @@
1.31 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.32 \<^rule_thm>\<open>separate_1_bdv_n\<close>(*,
1.33 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
1.34 - *****Rule.Thm ("add_divide_distrib",
1.35 - ***** ThmC.numerals_to_Free @{thm add_divide_distrib})
1.36 + *****\<^rule_thm>\<open>add_divide_distrib\<close>
1.37 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
1.38 ];
1.39 val simplify_Integral =
1.40 @@ -286,8 +282,7 @@
1.41 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.42 * \<^rule_thm>\<open>separate_1_bdv_n\<close>(*,
1.43 * (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
1.44 -* Rule.Thm ("add_divide_distrib",
1.45 -* ThmC.numerals_to_Free @{thm add_divide_distrib})
1.46 +* \<^rule_thm>\<open>add_divide_distrib\<close>
1.47 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
1.48 * ]),
1.49 * \<^rule_eval>\<open>divide\<close> (eval_cancel "#divide_e")
2.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 12 18:06:27 2021 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 12 18:22:07 2021 +0200
2.3 @@ -31,7 +31,7 @@
2.4 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
2.5 rules =
2.6 [
2.7 - Rule.Thm ("rule4", @{thm rule4})
2.8 + \<^rule_thm>\<open>rule4\<close>
2.9 ],
2.10 scr = Rule.Empty_Prog});
2.11 \<close>
2.12 @@ -126,9 +126,9 @@
2.13 (*2nd NTH_CONS pushes n+-1 into asms*)
2.14 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
2.15 srls = Rule_Set.Empty, calc = [], errpatts = [],
2.16 - rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
2.17 + rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
2.18 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
2.19 - Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
2.20 + \<^rule_thm>\<open>NTH_NIL\<close>,
2.21 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
2.22 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
2.23 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
3.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sat Jun 12 18:06:27 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sat Jun 12 18:22:07 2021 +0200
3.3 @@ -745,11 +745,9 @@
3.4 \<^rule_thm>\<open>real_plus_minus_binom2_p_p\<close>,
3.5 (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
3.6
3.7 - Rule.Thm ("real_add_mult_distrib_poly",
3.8 - ThmC.numerals_to_Free @{thm real_add_mult_distrib_poly}),
3.9 + \<^rule_thm>\<open>real_add_mult_distrib_poly\<close>,
3.10 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
3.11 - Rule.Thm("real_add_mult_distrib2_poly",
3.12 - ThmC.numerals_to_Free @{thm real_add_mult_distrib2_poly}),
3.13 + \<^rule_thm>\<open>real_add_mult_distrib2_poly\<close>,
3.14 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
3.15
3.16 \<^rule_thm>\<open>realpow_multI_poly\<close>,
3.17 @@ -773,12 +771,10 @@
3.18
3.19 \<^rule_thm>\<open>realpow_plus_1\<close>,
3.20 (*"r * r \<up> n = r \<up> (n + 1)"*)
3.21 - Rule.Thm ("realpow_plus_1_assoc_l",
3.22 - ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l}),
3.23 + \<^rule_thm>\<open>realpow_plus_1_assoc_l\<close>,
3.24 (*"r * (r \<up> m * s) = r \<up> (1 + m) * s"*)
3.25 (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a \<up> 2*(a*b) *)
3.26 - Rule.Thm ("realpow_plus_1_assoc_l2",
3.27 - ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l2}),
3.28 + \<^rule_thm>\<open>realpow_plus_1_assoc_l2\<close>,
3.29 (*"r \<up> m * (r * s) = r \<up> (1 + m) * s"*)
3.30
3.31 \<^rule_thm_sym>\<open>realpow_addI\<close>,
3.32 @@ -895,11 +891,9 @@
3.33 (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
3.34 \<^rule_thm>\<open>real_minus_binom_pow2_p\<close>,
3.35 (*"(a - b) \<up> 2 = a \<up> 2 + -2*a*b + b \<up> 2"*)
3.36 - Rule.Thm ("real_plus_minus_binom1_p",
3.37 - ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p}),
3.38 + \<^rule_thm>\<open>real_plus_minus_binom1_p\<close>,
3.39 (*"(a + b)*(a - b) = a \<up> 2 + -1*b \<up> 2"*)
3.40 - Rule.Thm ("real_plus_minus_binom2_p",
3.41 - ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p}),
3.42 + \<^rule_thm>\<open>real_plus_minus_binom2_p\<close>,
3.43 (*"(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
3.44
3.45 \<^rule_thm>\<open>minus_minus\<close>,
3.46 @@ -909,8 +903,7 @@
3.47 \<^rule_thm_sym>\<open>real_mult_minus1\<close>
3.48 (*- ?z = "-1 * ?z"*)
3.49
3.50 - (*Rule.Thm ("real_minus_add_distrib",
3.51 - ThmC.numerals_to_Free @{thm real_minus_add_distrib}),*)
3.52 + (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*)
3.53 (*"- (?x + ?y) = - ?x + - ?y"*)
3.54 (*\<^rule_thm>\<open>real_diff_plus\<close>*)
3.55 (*"a - b = a + -b"*)
3.56 @@ -968,11 +961,9 @@
3.57 (*"1 * z = z"*)
3.58 (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*)
3.59 (*"-1 * z = - z"*)
3.60 - Rule.Thm ("minus_mult_left",
3.61 - ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})),
3.62 + Rule.Thm ("minus_mult_left", ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})),
3.63 (*- (?x * ?y) = "- ?x * ?y"*)
3.64 - (*Rule.Thm ("real_minus_mult_cancel",
3.65 - ThmC.numerals_to_Free @{thm real_minus_mult_cancel}),
3.66 + (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>,
3.67 (*"- ?x * - ?y = ?x * ?y"*)---*)
3.68 \<^rule_thm>\<open>mult_zero_left\<close>,
3.69 (*"0 * z = 0"*)
3.70 @@ -1289,23 +1280,17 @@
3.71 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
3.72 ("POWER", ("Transcendental.powr", eval_binop "#power_"))
3.73 ], errpatts = [],
3.74 - rules = [Rule.Thm ("real_plus_binom_pow2",
3.75 - ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
3.76 + rules = [\<^rule_thm>\<open>real_plus_binom_pow2\<close>,
3.77 (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
3.78 - Rule.Thm ("real_plus_binom_times",
3.79 - ThmC.numerals_to_Free @{thm real_plus_binom_times}),
3.80 + \<^rule_thm>\<open>real_plus_binom_times\<close>,
3.81 (*"(a + b)*(a + b) = ...*)
3.82 - Rule.Thm ("real_minus_binom_pow2",
3.83 - ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
3.84 + \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
3.85 (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
3.86 - Rule.Thm ("real_minus_binom_times",
3.87 - ThmC.numerals_to_Free @{thm real_minus_binom_times}),
3.88 + \<^rule_thm>\<open>real_minus_binom_times\<close>,
3.89 (*"(a - b)*(a - b) = ...*)
3.90 - Rule.Thm ("real_plus_minus_binom1",
3.91 - ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),
3.92 + \<^rule_thm>\<open>real_plus_minus_binom1\<close>,
3.93 (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
3.94 - Rule.Thm ("real_plus_minus_binom2",
3.95 - ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),
3.96 + \<^rule_thm>\<open>real_plus_minus_binom2\<close>,
3.97 (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
3.98 (*RL 020915*)
3.99 \<^rule_thm>\<open>real_pp_binom_times\<close>,
3.100 @@ -1320,8 +1305,7 @@
3.101 (*(a*b) \<up> n = a \<up> n * b \<up> n*)
3.102 \<^rule_thm>\<open>real_plus_binom_pow3\<close>,
3.103 (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)
3.104 - Rule.Thm ("real_minus_binom_pow3",
3.105 - ThmC.numerals_to_Free @{thm real_minus_binom_pow3}),
3.106 + \<^rule_thm>\<open>real_minus_binom_pow3\<close>,
3.107 (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)
3.108
3.109
3.110 @@ -1345,8 +1329,7 @@
3.111 \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"),
3.112 (*\<^rule_thm>\<open>mult.commute\<close>,
3.113 (*AC-rewriting*)
3.114 - Rule.Thm ("real_mult_left_commute",
3.115 - ThmC.numerals_to_Free @{thm real_mult_left_commute}),
3.116 + \<^rule_thm>\<open>real_mult_left_commute\<close>,
3.117 \<^rule_thm>\<open>mult.assoc\<close>,
3.118 \<^rule_thm>\<open>add.commute\<close>,
3.119 \<^rule_thm>\<open>add.left_commute\<close>,
3.120 @@ -1363,14 +1346,12 @@
3.121
3.122 \<^rule_thm>\<open>real_num_collect\<close>,
3.123 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
3.124 - Rule.Thm ("real_num_collect_assoc",
3.125 - ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
3.126 + \<^rule_thm>\<open>real_num_collect_assoc\<close>,
3.127 (*"[| l is_const; m is_const |] ==>
3.128 l * n + (m * n + k) = (l + m) * n + k"*)
3.129 \<^rule_thm>\<open>real_one_collect\<close>,
3.130 (*"m is_const ==> n + m * n = (1 + m) * n"*)
3.131 - Rule.Thm ("real_one_collect_assoc",
3.132 - ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
3.133 + \<^rule_thm>\<open>real_one_collect_assoc\<close>,
3.134 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
3.135
3.136 \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
4.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sat Jun 12 18:06:27 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sat Jun 12 18:22:07 2021 +0200
4.3 @@ -439,9 +439,7 @@
4.4 erls = PolyEq_erls,
4.5 srls = Rule_Set.Empty,
4.6 calc = [], errpatts = [],
4.7 - rules = [\<^rule_thm>\<open>d0_true\<close>,
4.8 - Rule.Thm("d0_false",ThmC.numerals_to_Free @{thm d0_false})
4.9 - ],
4.10 + rules = [\<^rule_thm>\<open>d0_true\<close>, \<^rule_thm>\<open>d0_false\<close>],
4.11 scr = Rule.Empty_Prog
4.12 });
4.13
4.14 @@ -1305,8 +1303,7 @@
4.15 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
4.16 \<^rule_thm>\<open>separate_1_bdv_n\<close>,
4.17 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
4.18 - Rule.Thm ("add_divide_distrib",
4.19 - ThmC.numerals_to_Free @{thm add_divide_distrib})
4.20 + \<^rule_thm>\<open>add_divide_distrib\<close>
4.21 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
4.22 WN051031 DOES NOT BELONG TO HERE*)
4.23 ];
5.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sat Jun 12 18:06:27 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sat Jun 12 18:22:07 2021 +0200
5.3 @@ -660,11 +660,9 @@
5.4 (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
5.5 and does not commute a / b * c \<up> 2 !*)
5.6
5.7 - Rule.Thm ("divide_divide_eq_right",
5.8 - ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
5.9 + \<^rule_thm>\<open>divide_divide_eq_right\<close>,
5.10 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
5.11 - Rule.Thm ("divide_divide_eq_left",
5.12 - ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
5.13 + \<^rule_thm>\<open>divide_divide_eq_left\<close>,
5.14 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
5.15 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
5.16 ],
6.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sat Jun 12 18:06:27 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Sat Jun 12 18:22:07 2021 +0200
6.3 @@ -223,67 +223,49 @@
6.4 (* sqrt a sqrt b -> sqrt(ab) *)
6.5 \<^rule_thm>\<open>sqrt_times_root_2\<close>,
6.6 (* a sqrt b sqrt c -> a sqrt(bc) *)
6.7 - Rule.Thm("sqrt_square_equation_both_1",
6.8 - ThmC.numerals_to_Free @{thm sqrt_square_equation_both_1}),
6.9 + \<^rule_thm>\<open>sqrt_square_equation_both_1\<close>,
6.10 (* (sqrt a + sqrt b = sqrt c + sqrt d) ->
6.11 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
6.12 - Rule.Thm("sqrt_square_equation_both_2",
6.13 - ThmC.numerals_to_Free @{thm sqrt_square_equation_both_2}),
6.14 + \<^rule_thm>\<open>sqrt_square_equation_both_2\<close>,
6.15 (* (sqrt a - sqrt b = sqrt c + sqrt d) ->
6.16 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
6.17 - Rule.Thm("sqrt_square_equation_both_3",
6.18 - ThmC.numerals_to_Free @{thm sqrt_square_equation_both_3}),
6.19 + \<^rule_thm>\<open>sqrt_square_equation_both_3\<close>,
6.20 (* (sqrt a + sqrt b = sqrt c - sqrt d) ->
6.21 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
6.22 - Rule.Thm("sqrt_square_equation_both_4",
6.23 - ThmC.numerals_to_Free @{thm sqrt_square_equation_both_4}),
6.24 + \<^rule_thm>\<open>sqrt_square_equation_both_4\<close>,
6.25 (* (sqrt a - sqrt b = sqrt c - sqrt d) ->
6.26 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
6.27 - Rule.Thm("sqrt_isolate_l_add1",
6.28 - ThmC.numerals_to_Free @{thm sqrt_isolate_l_add1}),
6.29 + \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>,
6.30 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
6.31 - Rule.Thm("sqrt_isolate_l_add2",
6.32 - ThmC.numerals_to_Free @{thm sqrt_isolate_l_add2}),
6.33 + \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>,
6.34 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
6.35 - Rule.Thm("sqrt_isolate_l_add3",
6.36 - ThmC.numerals_to_Free @{thm sqrt_isolate_l_add3}),
6.37 + \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>,
6.38 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
6.39 - Rule.Thm("sqrt_isolate_l_add4",
6.40 - ThmC.numerals_to_Free @{thm sqrt_isolate_l_add4}),
6.41 + \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>,
6.42 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
6.43 - Rule.Thm("sqrt_isolate_l_add5",
6.44 - ThmC.numerals_to_Free @{thm sqrt_isolate_l_add5}),
6.45 + \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>,
6.46 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
6.47 - Rule.Thm("sqrt_isolate_l_add6",
6.48 - ThmC.numerals_to_Free @{thm sqrt_isolate_l_add6}),
6.49 + \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>,
6.50 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
6.51 (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
6.52 (* b*sqrt(x) = d sqrt(x) d/b *)
6.53 - Rule.Thm("sqrt_isolate_r_add1",
6.54 - ThmC.numerals_to_Free @{thm sqrt_isolate_r_add1}),
6.55 + \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>,
6.56 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
6.57 - Rule.Thm("sqrt_isolate_r_add2",
6.58 - ThmC.numerals_to_Free @{thm sqrt_isolate_r_add2}),
6.59 + \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>,
6.60 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
6.61 - Rule.Thm("sqrt_isolate_r_add3",
6.62 - ThmC.numerals_to_Free @{thm sqrt_isolate_r_add3}),
6.63 + \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>,
6.64 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
6.65 - Rule.Thm("sqrt_isolate_r_add4",
6.66 - ThmC.numerals_to_Free @{thm sqrt_isolate_r_add4}),
6.67 + \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>,
6.68 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
6.69 - Rule.Thm("sqrt_isolate_r_add5",
6.70 - ThmC.numerals_to_Free @{thm sqrt_isolate_r_add5}),
6.71 + \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>,
6.72 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
6.73 - Rule.Thm("sqrt_isolate_r_add6",
6.74 - ThmC.numerals_to_Free @{thm sqrt_isolate_r_add6}),
6.75 + \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>,
6.76 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
6.77 (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
6.78 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
6.79 - Rule.Thm("sqrt_square_equation_left_1",
6.80 - ThmC.numerals_to_Free @{thm sqrt_square_equation_left_1}),
6.81 + \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>,
6.82 (* sqrt(x)=b -> x=b^2 *)
6.83 - Rule.Thm("sqrt_square_equation_left_2",
6.84 - ThmC.numerals_to_Free @{thm sqrt_square_equation_left_2}),
6.85 + \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>,
6.86 (* c*sqrt(x)=b -> c^2*x=b^2 *)
6.87 \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,
6.88 (* c/sqrt(x)=b -> c^2/x=b^2 *)
7.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy Sat Jun 12 18:06:27 2021 +0200
7.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy Sat Jun 12 18:22:07 2021 +0200
7.3 @@ -2,7 +2,7 @@
7.4
7.5 ML \<open>val test_list_rls =
7.6 Rule_Set.append_rules "test_list_rls" Rule_Set.empty
7.7 - [Rule.Thm ("refl", @{thm refl}), Rule.Thm ("subst", @{thm subst})]\<close>
7.8 + [\<^rule_thm>\<open>refl\<close>, \<^rule_thm>\<open>subst\<close>]\<close>
7.9
7.10 setup \<open>Test_KEStore_Elems.add_rlss
7.11 [("test_list_rls", (Context.theory_name @{theory}, (*already added in Thy_1.thy*)
8.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy Sat Jun 12 18:06:27 2021 +0200
8.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy Sat Jun 12 18:22:07 2021 +0200
8.3 @@ -1,7 +1,7 @@
8.4 theory Thy_2b imports Thy_1 begin
8.5
8.6 ML \<open>val test_list_rls =
8.7 - Rule_Set.append_rules "test_list_rls" Rule_Set.empty [Rule.Thm ("False_def", @{thm False_def})]\<close>
8.8 + Rule_Set.append_rules "test_list_rls" Rule_Set.empty [\<^rule_thm>\<open>False_def\<close>]\<close>
8.9
8.10 setup \<open>Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory},
8.11 test_list_rls))]\<close>
9.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy Sat Jun 12 18:06:27 2021 +0200
9.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy Sat Jun 12 18:22:07 2021 +0200
9.3 @@ -1,7 +1,7 @@
9.4 theory Thy_3 imports Thy_2 Thy_2b begin
9.5
9.6 ML \<open>val test_list_rls =
9.7 - Rule_Set.append_rules "test_list_rls" Rule_Set.empty [Rule.Thm ("not_def", @{thm not_def})]\<close>
9.8 + Rule_Set.append_rules "test_list_rls" Rule_Set.empty [\<^rule_thm>\<open>not_def\<close>]\<close>
9.9
9.10 setup \<open>Test_KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*)
9.11 [("test_list_rls", (Context.theory_name @{theory}, test_list_rls))]\<close>
10.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Sat Jun 12 18:06:27 2021 +0200
10.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Sat Jun 12 18:22:07 2021 +0200
10.3 @@ -221,7 +221,7 @@
10.4 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
10.5 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
10.6 (*compare Prog_Expr.*)
10.7 -val prog = Auto_Prog.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})]
10.8 +val prog = Auto_Prog.rules2scr_Rls @{theory} [\<^rule_thm>\<open>thm111\<close>, \<^rule_thm>\<open>refl\<close>]
10.9 ;
10.10 writeln (UnparseC.term_in_thy @{theory} prog);
10.11 (*auto_generated t_t =