1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Apr 01 19:20:05 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Sat Apr 04 12:11:32 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.append_rls "LinEq_prls" Rule.e_rls 
     1.8 +  Rule_Set.append_rls "LinEq_prls" Rule_Set.e_rls 
     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.append_rls "LinEq_crls" poly_crls
    1.17 +   Rule_Set.append_rls "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.append_rls "LinEq_erls" Poly_erls
    1.26 +   Rule_Set.append_rls "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 @@ -69,10 +69,10 @@
    1.31  ML \<open>
    1.32      
    1.33  val LinPoly_simplify = prep_rls'(
    1.34 -  Rule.Rls {id = "LinPoly_simplify", preconds = [], 
    1.35 +  Rule_Set.Rls {id = "LinPoly_simplify", preconds = [], 
    1.36         rew_ord = ("termlessI",termlessI), 
    1.37         erls = LinEq_erls, 
    1.38 -       srls = Rule.Erls, 
    1.39 +       srls = Rule_Set.Erls, 
    1.40         calc = [], errpatts = [],
    1.41         rules = [
    1.42  		Rule.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
    1.43 @@ -93,10 +93,10 @@
    1.44  
    1.45  (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
    1.46  val LinEq_simplify = prep_rls'(
    1.47 -Rule.Rls {id = "LinEq_simplify", preconds = [],
    1.48 +Rule_Set.Rls {id = "LinEq_simplify", preconds = [],
    1.49       rew_ord = ("e_rew_ord", Rule.e_rew_ord),
    1.50       erls = LinEq_erls,
    1.51 -     srls = Rule.Erls,
    1.52 +     srls = Rule_Set.Erls,
    1.53       calc = [], errpatts = [],
    1.54       rules = [
    1.55  	      Rule.Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}), 
    1.56 @@ -129,7 +129,7 @@
    1.57  setup \<open>KEStore_Elems.add_mets
    1.58      [Specify.prep_met thy "met_eqlin" [] Celem.e_metID
    1.59        (["LinEq"], [],
    1.60 -        {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
    1.61 +        {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.e_rls, prls = Rule_Set.e_rls,
    1.62            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.63          @{thm refl})]
    1.64  \<close>
    1.65 @@ -156,7 +156,7 @@
    1.66          [("#Given", ["equality e_e", "solveFor v_v"]),
    1.67            ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),
    1.68            ("#Find",  ["solutions v_v'i'"])],
    1.69 -        {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule.e_rls, prls = LinEq_prls, calc = [],
    1.70 +        {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule_Set.e_rls, prls = LinEq_prls, calc = [],
    1.71            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.72          @{thm solve_linear_equation.simps})]
    1.73  \<close>