src/Tools/isac/Knowledge/Base_Tools.thy
changeset 60385 d3a3cc2f0382
parent 60384 2b6e73df4e5d
child 60405 d4ebe139100d
     1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Aug 18 11:35:24 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Aug 18 16:03:08 2021 +0200
     1.3 @@ -29,7 +29,6 @@
     1.4  calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
     1.5  calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
     1.6  calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close>
     1.7 -calculation is_const = \<open>Prog_Expr.eval_const "#is_const_"\<close>
     1.8  calculation le (less) = \<open>Prog_Expr.eval_equ "#less_"\<close>
     1.9  calculation leq (less_eq) = \<open>Prog_Expr.eval_equ "#less_equal_"\<close>
    1.10  calculation ident = \<open>Prog_Expr.eval_ident "#ident_"\<close>
    1.11 @@ -82,7 +81,7 @@
    1.12  	\<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
    1.13  	
    1.14  	\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
    1.15 -	\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
    1.16 +	\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
    1.17  	\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
    1.18  	\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
    1.19  \<close>
    1.20 @@ -108,7 +107,7 @@
    1.21   	\<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
    1.22   	
    1.23   	\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
    1.24 - 	\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
    1.25 +	\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
    1.26   	\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
    1.27   	\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
    1.28  \<close>