1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Fri May 07 13:23:24 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Fri May 07 18:12:51 2021 +0200
     1.3 @@ -25,11 +25,11 @@
     1.4  subsection \<open>setup for ML-functions\<close>
     1.5  text \<open>required by "eval_binop" below\<close>
     1.6  setup \<open>KEStore_Elems.add_calcs
     1.7 -  [ ("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_")),
     1.8 -    ("some_occur_in", ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_")),
     1.9 -    ("is_atom", ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_")),
    1.10 -    ("is_even", ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_")),
    1.11 -    ("is_const", ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")),
    1.12 +  [ ("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "#occurs_in_")),
    1.13 +    ("some_occur_in", ("Prog_Expr.some_occur_in", Prog_Expr.eval_some_occur_in "#some_occur_in_")),
    1.14 +    ("is_atom", ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_")),
    1.15 +    ("is_even", ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_")),
    1.16 +    ("is_const", ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")),
    1.17      ("le", ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")),
    1.18      ("leq", ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_")),
    1.19      ("ident", ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")),
    1.20 @@ -88,8 +88,8 @@
    1.21  		Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
    1.22  		
    1.23  		Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),    
    1.24 -		Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
    1.25 -		Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
    1.26 +		Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
    1.27 +		Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),    
    1.28  		Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
    1.29  \<close>
    1.30  
    1.31 @@ -114,8 +114,8 @@
    1.32  		Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
    1.33  		
    1.34  		Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),    
    1.35 -		Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
    1.36 -		Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
    1.37 +		Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
    1.38 +		Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),    
    1.39  		Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
    1.40  \<close>
    1.41  
    1.42 @@ -151,4 +151,8 @@
    1.43  setup \<open>KEStore_Elems.add_rlss
    1.44    [("prog_expr", (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} prog_expr))]\<close>
    1.45  
    1.46 +ML \<open>
    1.47 +\<close> ML \<open>
    1.48 +\<close> ML \<open>
    1.49 +\<close>
    1.50  end