1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Jun 21 16:18:27 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Jun 21 20:06:12 2021 +0200
     1.3 @@ -24,22 +24,21 @@
     1.4  
     1.5  subsection \<open>setup for ML-functions\<close>
     1.6  text \<open>required by "eval_binop" below\<close>
     1.7 -setup \<open>KEStore_Elems.add_calcs
     1.8 -  [ ("occurs_in", (\<^const_name>\<open>occurs_in\<close>, Prog_Expr.eval_occurs_in "#occurs_in_")),
     1.9 -    ("some_occur_in", (\<^const_name>\<open>some_occur_in\<close>, Prog_Expr.eval_some_occur_in "#some_occur_in_")),
    1.10 -    ("is_atom", (\<^const_name>\<open>is_atom\<close>, Prog_Expr.eval_is_atom "#is_atom_")),
    1.11 -    ("is_even", (\<^const_name>\<open>is_even\<close>, Prog_Expr.eval_is_even "#is_even_")),
    1.12 -    ("is_const", (\<^const_name>\<open>is_const\<close>, Prog_Expr.eval_const "#is_const_")),
    1.13 -    ("le", (\<^const_name>\<open>less\<close>, Prog_Expr.eval_equ "#less_")),
    1.14 -    ("leq", (\<^const_name>\<open>less_eq\<close>, Prog_Expr.eval_equ "#less_equal_")),
    1.15 -    ("ident", (\<^const_name>\<open>ident\<close>, Prog_Expr.eval_ident "#ident_")),
    1.16 -    ("equal", (\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")),
    1.17 -    ("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
    1.18 -    ("MINUS", (\<^const_name>\<open>minus\<close>, (**)eval_binop "#sub_")),
    1.19 -    ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
    1.20 -    ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
    1.21 -    ("POWER",(\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_")),
    1.22 -    ("boollist2sum", (\<^const_name>\<open>boollist2sum\<close>, Prog_Expr.eval_boollist2sum ""))]\<close>
    1.23 +calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close>
    1.24 +calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
    1.25 +calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
    1.26 +calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close>
    1.27 +calculation is_const = \<open>Prog_Expr.eval_const "#is_const_"\<close>
    1.28 +calculation le (less) = \<open>Prog_Expr.eval_equ "#less_"\<close>
    1.29 +calculation leq (less_eq) = \<open>Prog_Expr.eval_equ "#less_equal_"\<close>
    1.30 +calculation ident = \<open>Prog_Expr.eval_ident "#ident_"\<close>
    1.31 +calculation equal (HOL.eq) = \<open>Prog_Expr.eval_equal "#equal_"\<close>
    1.32 +calculation PLUS (plus) = \<open>(**)eval_binop "#add_"\<close>
    1.33 +calculation MINUS (minus) = \<open>(**)eval_binop "#sub_"\<close>
    1.34 +calculation TIMES (times) = \<open>(**)eval_binop "#mult_"\<close>
    1.35 +calculation DIVIDE (divide) = \<open>Prog_Expr.eval_cancel "#divide_e"\<close>
    1.36 +calculation POWER (powr) = \<open>(**)eval_binop "#power_"\<close>
    1.37 +calculation boollist2sum = \<open>Prog_Expr.eval_boollist2sum ""\<close>
    1.38  
    1.39  subsection \<open>rewrite-order for rule-sets\<close>
    1.40  ML \<open>