1.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Apr 15 11:11:54 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Apr 15 11:37:43 2020 +0200
     1.3 @@ -71,13 +71,13 @@
     1.4  ML \<open>
     1.5  val RootRatEq_prls = 
     1.6    Rule_Set.append_rules "RootRatEq_prls" Rule_Set.empty
     1.7 -		[Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
     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 ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in ""),
    1.12 -     Rule.Num_Calc ("RootRatEq.is'_rootRatAddTerm'_in", eval_is_rootRatAddTerm_in ""),
    1.13 -     Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
    1.14 +		[Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
    1.15 +     Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
    1.16 +     Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs ""),
    1.17 +     Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""),
    1.18 +     Rule.Eval ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in ""),
    1.19 +     Rule.Eval ("RootRatEq.is'_rootRatAddTerm'_in", eval_is_rootRatAddTerm_in ""),
    1.20 +     Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
    1.21       Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
    1.22       Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
    1.23       Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
    1.24 @@ -115,7 +115,7 @@
    1.25                                     ( (a = d + e/f) = ( (a - d) * f = e )) *)
    1.26       Rule.Thm("rootrat_equation_right_2",ThmC.numerals_to_Free @{thm rootrat_equation_right_2})
    1.27  	(* [|f is_rootTerm_in bdv|] ==> ( (a =  e/f) = ( a  * f = e ))*)
    1.28 -     ], scr = Rule.EmptyScr});
    1.29 +     ], scr = Rule.Empty_Prog});
    1.30  \<close>
    1.31  setup \<open>KEStore_Elems.add_rlss
    1.32    [("RooRatEq_erls", (Context.theory_name @{theory}, RooRatEq_erls)),