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