1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Oct 31 18:28:36 2022 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Nov 07 17:37:20 2022 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4      \<^rule_thm>\<open>and_false\<close>,
     1.5      \<^rule_thm>\<open>or_true\<close>,
     1.6      \<^rule_thm>\<open>or_false\<close>];
     1.7 -(* ----- erls ----- *)
     1.8 +(* ----- asm_rls ----- *)
     1.9  val LinEq_crls = 
    1.10     Rule_Set.append_rules "LinEq_crls" poly_crls
    1.11     [\<^rule_thm>\<open>real_assoc_1\<close>
    1.12 @@ -67,8 +67,8 @@
    1.13  val LinPoly_simplify = prep_rls'(
    1.14    Rule_Def.Repeat {id = "LinPoly_simplify", preconds = [], 
    1.15      rew_ord = ("termlessI",termlessI), 
    1.16 -    erls = LinEq_erls, 
    1.17 -    srls = Rule_Set.Empty, 
    1.18 +    asm_rls = LinEq_erls, 
    1.19 +    prog_rls = Rule_Set.Empty, 
    1.20      calc = [], errpatts = [],
    1.21      rules = [
    1.22        \<^rule_thm>\<open>real_assoc_1\<close>,
    1.23 @@ -80,7 +80,7 @@
    1.24         \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
    1.25         *)
    1.26        \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
    1.27 -    scr = Rule.Empty_Prog});
    1.28 +    program = Rule.Empty_Prog});
    1.29  \<close>
    1.30  rule_set_knowledge LinPoly_simplify = LinPoly_simplify
    1.31  ML \<open>
    1.32 @@ -89,14 +89,14 @@
    1.33  val LinEq_simplify = prep_rls'(
    1.34    Rule_Def.Repeat {id = "LinEq_simplify", preconds = [],
    1.35      rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
    1.36 -    erls = LinEq_erls,
    1.37 -    srls = Rule_Set.Empty,
    1.38 +    asm_rls = LinEq_erls,
    1.39 +    prog_rls = Rule_Set.Empty,
    1.40      calc = [], errpatts = [],
    1.41      rules = [
    1.42  	     \<^rule_thm>\<open>lin_isolate_add1\<close>, (* a+bx=0 -> bx=-a *)
    1.43  	     \<^rule_thm>\<open>lin_isolate_add2\<close>, (* a+ x=0 ->  x=-a *)
    1.44  	     \<^rule_thm>\<open>lin_isolate_div\<close> (*   bx=c -> x=c/b *)],
    1.45 -    scr = Rule.Empty_Prog});
    1.46 +    program = Rule.Empty_Prog});
    1.47  \<close>
    1.48  rule_set_knowledge LinEq_simplify = LinEq_simplify
    1.49  
    1.50 @@ -117,8 +117,8 @@
    1.51  
    1.52  (*-------------- methods------------------------------------------------------*)
    1.53  method met_eqlin : "LinEq" =
    1.54 -  \<open>{rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.55 -    crls = LinEq_crls, errpats = [], nrls = norm_Poly}\<close>
    1.56 +  \<open>{rew_ord = "tless_true",rls' = Atools_erls,calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty,
    1.57 +    crls = LinEq_crls, errpats = [], rew_rls = norm_Poly}\<close>
    1.58      (* ansprechen mit ["LinEq", "solve_univar_equation"] *)
    1.59  
    1.60  partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"
    1.61 @@ -138,8 +138,8 @@
    1.62      Or_to_List e_e)"
    1.63  
    1.64  method met_eq_lin : "LinEq/solve_lineq_equation" =
    1.65 -  \<open>{rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule_Set.empty, prls = LinEq_prls, calc = [],
    1.66 -    crls = LinEq_crls, errpats = [], nrls = norm_Poly}\<close>
    1.67 +  \<open>{rew_ord = "termlessI", rls' = LinEq_erls, prog_rls = Rule_Set.empty, where_rls = LinEq_prls, calc = [],
    1.68 +    crls = LinEq_crls, errpats = [], rew_rls = norm_Poly}\<close>
    1.69    Program: solve_linear_equation.simps
    1.70    Given: "equality e_e" "solveFor v_v"
    1.71    Where: "Not ((lhs e_e) is_polyrat_in v_v)" "((lhs e_e)  has_degree_in v_v) = 1"