1.1 --- a/src/Tools/isac/Knowledge/Root.thy Mon Oct 31 18:28:36 2022 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Root.thy Mon Nov 07 17:37:20 2022 +0100
1.3 @@ -190,7 +190,7 @@
1.4 val make_rooteq = prep_rls'(
1.5 Rule_Def.Repeat{id = "make_rooteq", preconds = []:term list,
1.6 rew_ord = ("sqrt_right", sqrt_right false \<^theory>),
1.7 - erls = Atools_erls, srls = Rule_Set.Empty,
1.8 + asm_rls = Atools_erls, prog_rls = Rule_Set.Empty,
1.9 calc = [], errpatts = [],
1.10 rules = [
1.11 \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*)
1.12 @@ -225,7 +225,7 @@
1.13 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
1.14 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
1.15 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
1.16 - scr = Rule.Empty_Prog});
1.17 + program = Rule.Empty_Prog});
1.18 \<close>
1.19 rule_set_knowledge make_rooteq = make_rooteq
1.20 ML \<open>
1.21 @@ -235,7 +235,7 @@
1.22 val expand_rootbinoms = prep_rls'(
1.23 Rule_Def.Repeat {
1.24 id = "expand_rootbinoms", preconds = [], rew_ord = ("termlessI",termlessI),
1.25 - erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.26 + asm_rls = Atools_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.27 rules = [
1.28 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
1.29 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*)
1.30 @@ -276,7 +276,7 @@
1.31 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.32 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
1.33 \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
1.34 - scr = Rule.Empty_Prog});
1.35 + program = Rule.Empty_Prog});
1.36 \<close>
1.37 rule_set_knowledge expand_rootbinoms = expand_rootbinoms
1.38 ML \<open>