1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Apr 15 11:11:54 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed Apr 15 11:37:43 2020 +0200
     1.3 @@ -27,14 +27,14 @@
     1.4  
     1.5  val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
     1.6    Rule_Set.append_rules "LinEq_prls" Rule_Set.empty 
     1.7 -	     [Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
     1.8 -	      Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
     1.9 -	      Rule.Num_Calc ("Prog_Expr.lhs"    , Prog_Expr.eval_lhs ""),
    1.10 -	      Rule.Num_Calc ("Prog_Expr.rhs"    , Prog_Expr.eval_rhs ""),
    1.11 -	      Rule.Num_Calc ("Poly.has'_degree'_in", eval_has_degree_in ""),
    1.12 - 	      Rule.Num_Calc ("Poly.is'_polyrat'_in", eval_is_polyrat_in ""),
    1.13 -	      Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
    1.14 -	      Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
    1.15 +	     [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
    1.16 +	      Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
    1.17 +	      Rule.Eval ("Prog_Expr.lhs"    , Prog_Expr.eval_lhs ""),
    1.18 +	      Rule.Eval ("Prog_Expr.rhs"    , Prog_Expr.eval_rhs ""),
    1.19 +	      Rule.Eval ("Poly.has'_degree'_in", eval_has_degree_in ""),
    1.20 + 	      Rule.Eval ("Poly.is'_polyrat'_in", eval_is_polyrat_in ""),
    1.21 +	      Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
    1.22 +	      Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
    1.23  	      Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
    1.24  	      Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
    1.25  	      Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
    1.26 @@ -48,8 +48,8 @@
    1.27     [Rule.Thm  ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1})
    1.28      (*		
    1.29       Don't use
    1.30 -     Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
    1.31 -     Rule.Num_Calc ("Prog_Expr.pow" , (**)eval_binop "#power_"),
    1.32 +     Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
    1.33 +     Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_"),
    1.34       *)
    1.35      ];
    1.36  
    1.37 @@ -59,8 +59,8 @@
    1.38     [Rule.Thm  ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1})
    1.39      (*		
    1.40       Don't use
    1.41 -     Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
    1.42 -     Rule.Num_Calc ("Prog_Expr.pow" , (**)eval_binop "#power_"),
    1.43 +     Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
    1.44 +     Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_"),
    1.45       *)
    1.46      ];
    1.47  \<close>
    1.48 @@ -76,16 +76,16 @@
    1.49         calc = [], errpatts = [],
    1.50         rules = [
    1.51  		Rule.Thm  ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1}),
    1.52 -		Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.53 -		Rule.Num_Calc ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
    1.54 -		Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
    1.55 +		Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.56 +		Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
    1.57 +		Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
    1.58  		(*  Dont use  
    1.59 -		 Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),		
    1.60 -		 Rule.Num_Calc ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
    1.61 +		 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),		
    1.62 +		 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
    1.63  		 *)
    1.64 -		Rule.Num_Calc ("Prog_Expr.pow" , (**)eval_binop "#power_")
    1.65 +		Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_")
    1.66  		],
    1.67 -       scr = Rule.EmptyScr});
    1.68 +       scr = Rule.Empty_Prog});
    1.69  \<close>
    1.70  setup \<open>KEStore_Elems.add_rlss 
    1.71    [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))]\<close>
    1.72 @@ -106,7 +106,7 @@
    1.73  	      Rule.Thm("lin_isolate_div",ThmC.numerals_to_Free @{thm lin_isolate_div})    
    1.74  	      (*   bx=c -> x=c/b *)  
    1.75  	      ],
    1.76 -     scr = Rule.EmptyScr});
    1.77 +     scr = Rule.Empty_Prog});
    1.78  \<close>
    1.79  setup \<open>KEStore_Elems.add_rlss 
    1.80    [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))]\<close>