diff -r 2b6e73df4e5d -r d3a3cc2f0382 src/Tools/isac/ProgLang/Prog_Expr.thy
--- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 18 11:35:24 2021 +0200
+++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 18 16:03:08 2021 +0200
@@ -31,9 +31,6 @@
   abs              :: "real => real"            ("(|| _ ||)")
   (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
   absset           :: "real set => real"        ("(||| _ |||)")
-  (*is numeral constant ?*)
-  is_const        :: "real => bool"            ("_ is'_const" 10)
-  (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
   is_atom         :: "real => bool"            ("_ is'_atom" 10)
   is_num         :: "real => bool"             ("_ is'_num" 10)
   is_even         :: "real => bool"            ("_ is'_even" 10)
@@ -315,15 +312,15 @@
     else NONE
   | eval_is_even _ _ _ _ = NONE; 
 
-(*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
-fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
+(*("is_num",("Prog_Expr.is_num", Prog_Expr.eval_is_num "#is_num_"))*)
+fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
     (*TODO get rid of this special case*)
     SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
-  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const _)) _ =
+  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ Const _)) _ =
     SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
-  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ n)) _ =
+  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_num\<close>, _) $ n)) _ =
 	   if TermC.is_num n
 	   then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))