1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 18 16:03:08 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 18 16:46:22 2021 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    abs              :: "real => real"            ("(|| _ ||)")
     1.5    (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
     1.6    absset           :: "real set => real"        ("(||| _ |||)")
     1.7 +  is_const        :: "real => bool"            ("_ is'_const" 10) (* re-establish intermed.TOODOO *)
     1.8    is_atom         :: "real => bool"            ("_ is'_atom" 10)
     1.9    is_num         :: "real => bool"             ("_ is'_num" 10)
    1.10    is_even         :: "real => bool"            ("_ is'_even" 10)
    1.11 @@ -312,15 +313,15 @@
    1.12      else NONE
    1.13    | eval_is_even _ _ _ _ = NONE; 
    1.14  
    1.15 -(*("is_num",("Prog_Expr.is_num", Prog_Expr.eval_is_num "#is_num_"))*)
    1.16 -fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
    1.17 +(*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
    1.18 +fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
    1.19      (*TODO get rid of this special case*)
    1.20      SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
    1.21        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.22 -  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ Const _)) _ =
    1.23 +  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const _)) _ =
    1.24      SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
    1.25        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.26 -  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ n)) _ =
    1.27 +  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ n)) _ =
    1.28  	   if TermC.is_num n
    1.29  	   then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
    1.30         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))