1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  val thy = @{theory};
     1.5  
     1.6  val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
     1.7 -  Rule_Set.append_rls "LinEq_prls" Rule_Set.e_rls 
     1.8 +  Rule_Set.append_rules "LinEq_prls" Rule_Set.empty 
     1.9  	     [Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
    1.10  	      Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
    1.11  	      Rule.Num_Calc ("Prog_Expr.lhs"    , Prog_Expr.eval_lhs ""),
    1.12 @@ -44,7 +44,7 @@
    1.13                ];
    1.14  (* ----- erls ----- *)
    1.15  val LinEq_crls = 
    1.16 -   Rule_Set.append_rls "LinEq_crls" poly_crls
    1.17 +   Rule_Set.append_rules "LinEq_crls" poly_crls
    1.18     [Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1})
    1.19      (*		
    1.20       Don't use
    1.21 @@ -55,7 +55,7 @@
    1.22  
    1.23  (* ----- crls ----- *)
    1.24  val LinEq_erls = 
    1.25 -   Rule_Set.append_rls "LinEq_erls" Poly_erls
    1.26 +   Rule_Set.append_rules "LinEq_erls" Poly_erls
    1.27     [Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1})
    1.28      (*		
    1.29       Don't use
    1.30 @@ -129,7 +129,7 @@
    1.31  setup \<open>KEStore_Elems.add_mets
    1.32      [Specify.prep_met thy "met_eqlin" [] Celem.e_metID
    1.33        (["LinEq"], [],
    1.34 -        {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.e_rls, prls = Rule_Set.e_rls,
    1.35 +        {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.36            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.37          @{thm refl})]
    1.38  \<close>
    1.39 @@ -156,7 +156,7 @@
    1.40          [("#Given", ["equality e_e", "solveFor v_v"]),
    1.41            ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),
    1.42            ("#Find",  ["solutions v_v'i'"])],
    1.43 -        {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule_Set.e_rls, prls = LinEq_prls, calc = [],
    1.44 +        {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule_Set.empty, prls = LinEq_prls, calc = [],
    1.45            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.46          @{thm solve_linear_equation.simps})]
    1.47  \<close>