1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun Aug 01 14:39:03 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Aug 02 11:38:40 2021 +0200
     1.3 @@ -35,6 +35,7 @@
     1.4    is_const        :: "real => bool"            ("_ is'_const" 10)
     1.5    (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
     1.6    is_atom         :: "real => bool"            ("_ is'_atom" 10)
     1.7 +  is_num         :: "real => bool"             ("_ is'_num" 10)
     1.8    is_even         :: "real => bool"            ("_ is'_even" 10)
     1.9  		
    1.10    (* identity on term level*)
    1.11 @@ -68,6 +69,7 @@
    1.12      val some_occur_in: term list -> term -> bool
    1.13      val eval_some_occur_in: 'a -> string -> term -> 'b -> (string * term) option
    1.14      val eval_is_atom: string -> string -> term -> 'a -> (string * term) option
    1.15 +    val eval_is_num: string -> string -> term -> 'a -> (string * term) option
    1.16      val even: int -> bool
    1.17      val eval_is_even: string -> string -> term -> 'a -> (string * term) option
    1.18      val eval_const: string -> string -> term -> 'a -> (string * term) option
    1.19 @@ -287,6 +289,15 @@
    1.20  		  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.21    | eval_is_atom _ _ _ _ = NONE;
    1.22  
    1.23 +(*("is_num",("Prog_Expr.is_num", Prog_Expr.eval_is_num "#is_num_"))*)
    1.24 +fun eval_is_num (thmid:string) "Prog_Expr.is_num" (t as (Const _ $ arg)) _ = 
    1.25 +    if TermC.is_num arg
    1.26 +    then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "", 
    1.27 +			HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.28 +    else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "", 
    1.29 +		  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.30 +  | eval_is_num _ _ _ _ = NONE;
    1.31 +
    1.32  fun even i = (i div 2) * 2 = i;
    1.33  (*("is_even",("Prog_Expr.is_even", eval_is_even "#is_even_"))*)
    1.34  fun eval_is_even (thmid:string) "Prog_Expr.is_even" (t as (Const _ $ arg)) _ =