src/Tools/isac/Knowledge/Root.thy
changeset 60586 007ef64dbb08
parent 60567 bb3140a02f3d
child 60588 9a116f94c5a6
     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>