1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Sat Aug 21 18:58:33 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sun Aug 22 09:43:43 2021 +0200
     1.3 @@ -410,13 +410,11 @@
     1.4  val calc_rat_erls =
     1.5    prep_rls'
     1.6      (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
     1.7 -      erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.8 +      erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.9        rules = [
    1.10          \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
    1.11          \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
    1.12 -(*/----- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly -------\* )
    1.13          \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
    1.14 -( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
    1.15          \<^rule_thm>\<open>not_true\<close>,
    1.16          \<^rule_thm>\<open>not_false\<close>], 
    1.17        scr = Rule.Empty_Prog});
    1.18 @@ -654,6 +652,7 @@
    1.19      rules = [
    1.20        (*\<^rule_thm>\<open>divide_1\<close>, "?x / 1 = ?x" unnecessary.for normalform*)
    1.21  	    \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
    1.22 +	    \<^rule_thm>\<open>minus_zero\<close>, (*"- 0 = 0"*)
    1.23  	    (*\<^rule_thm>\<open>real_mult_minus1\<close>, "-1 * z = - z"*)
    1.24  	    (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>, "- ?x * - ?y = ?x * ?y"*)
    1.25