1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Sep 13 15:42:43 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Sep 13 16:01:48 2021 +0200
     1.3 @@ -667,19 +667,13 @@
     1.4        \<^rule_thm>\<open>division_ring_divide_zero\<close> (*"0 / ?x = 0"*)],
     1.5      scr = Rule.Empty_Prog});
     1.6  
     1.7 -\<close> ML \<open>
     1.8 -\<close> ML \<open>@{term "1 is_num"}\<close> (*.."Prog_Expr.is_num" IS KNOWN TOODOO*)
     1.9 -ML \<open>
    1.10  (*erls for calculate_Rational; 
    1.11    make local with FIXX@ME result:term *term list WN0609???SKMG*)
    1.12  val norm_rat_erls = prep_rls'(
    1.13    Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    1.14      erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.15      rules = [
    1.16 -      \<^rule_thm>\<open>refl\<close> (* ..DELETE, just to avoid ERROR fun #> not applicable to "[]"*)
    1.17 -(*/----- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly -------\* )
    1.18        \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")
    1.19 -( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
    1.20  ],
    1.21      scr = Rule.Empty_Prog});
    1.22