1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Aug 18 16:03:08 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Aug 18 16:46:22 2021 +0200
     1.3 @@ -41,6 +41,7 @@
     1.4  
     1.5    val is_atom: term -> bool
     1.6    val string_of_atom: term -> string
     1.7 +  val is_const: term -> bool   (* re-establish intermed.TOODOO *)
     1.8    val is_variable: term -> bool
     1.9    val is_bdv: string -> bool
    1.10    val is_bdv_subst: term -> bool
    1.11 @@ -298,7 +299,7 @@
    1.12  fun is_f_x (f $ x) = is_fun_id f andalso is_Free x
    1.13    | is_f_x _ = false;
    1.14  (* precondition: TermC.is_atom v andalso TermC.is_atom c *)
    1.15 -fun is_const (Const _) = true | is_const _ = false;
    1.16 +fun is_const (Const _) = true | is_const _ = false; (*TOODOO kept for strange code below*)
    1.17  fun variable_constant_pair (v, c) =
    1.18    if (is_variable v andalso (is_const c orelse is_num c)) orelse
    1.19       (is_variable c andalso (is_const v orelse is_num v))

     2.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Wed Aug 18 16:03:08 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Wed Aug 18 16:46:22 2021 +0200
     2.3 @@ -1320,10 +1320,10 @@
     2.4  ML \<open>@{term "1 is_num"}\<close> (*.."Prog_Expr.is_num" IS KNOWN TOODOO*)
     2.5  rule_set_knowledge
     2.6    norm_Poly = \<open>prep_rls' norm_Poly\<close> 
     2.7 -(*/---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------\* )
     2.8 +(*/---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------\*)
     2.9  and
    2.10    Poly_erls = \<open>prep_rls' Poly_erls\<close> (*FIXXXME:del with rls.rls'*) 
    2.11 -( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
    2.12 +(*\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
    2.13  and
    2.14    expand = \<open>prep_rls' expand\<close> and
    2.15    expand_poly = \<open>prep_rls' expand_poly\<close> and

     3.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 18 16:03:08 2021 +0200
     3.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 18 16:46:22 2021 +0200
     3.3 @@ -31,6 +31,7 @@
     3.4    abs              :: "real => real"            ("(|| _ ||)")
     3.5    (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
     3.6    absset           :: "real set => real"        ("(||| _ |||)")
     3.7 +  is_const        :: "real => bool"            ("_ is'_const" 10) (* re-establish intermed.TOODOO *)
     3.8    is_atom         :: "real => bool"            ("_ is'_atom" 10)
     3.9    is_num         :: "real => bool"             ("_ is'_num" 10)
    3.10    is_even         :: "real => bool"            ("_ is'_even" 10)
    3.11 @@ -312,15 +313,15 @@
    3.12      else NONE
    3.13    | eval_is_even _ _ _ _ = NONE; 
    3.14  
    3.15 -(*("is_num",("Prog_Expr.is_num", Prog_Expr.eval_is_num "#is_num_"))*)
    3.16 -fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
    3.17 +(*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
    3.18 +fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
    3.19      (*TODO get rid of this special case*)
    3.20      SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
    3.21        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    3.22 -  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ Const _)) _ =
    3.23 +  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const _)) _ =
    3.24      SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
    3.25        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    3.26 -  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ n)) _ =
    3.27 +  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ n)) _ =
    3.28  	   if TermC.is_num n
    3.29  	   then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
    3.30         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))