1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Aug 23 12:33:10 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Aug 23 14:24:06 2021 +0200
     1.3 @@ -650,7 +650,7 @@
     1.4    Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
     1.5      erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.6      rules = [
     1.7 -      (*\<^rule_thm>\<open>divide_1\<close>, "?x / 1 = ?x" unnecessary.for normalform*)
     1.8 +      \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
     1.9  	    \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
    1.10  	    \<^rule_thm>\<open>minus_zero\<close>, (*"- 0 = 0"*)
    1.11  	    (*\<^rule_thm>\<open>real_mult_minus1\<close>, "-1 * z = - z"*)
    1.12 @@ -711,7 +711,7 @@
    1.13      erls = Atools_erls, srls = Rule_Set.Empty,
    1.14      calc = [], errpatts = [],
    1.15      rules = [
    1.16 -      Rule.Rls_  norm_Rational_min,
    1.17 +      Rule.Rls_ norm_Rational_min,
    1.18  	    Rule.Rls_ discard_parentheses],
    1.19      scr = Rule.Empty_Prog});      
    1.20