1.1 --- a/src/Tools/isac/Knowledge/Atools.thy	Fri Oct 25 20:52:08 2013 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy	Fri Oct 25 20:58:28 2013 +0100
     1.3 @@ -670,25 +670,6 @@
     1.4        }:rls);
     1.5  *)
     1.6  "******* Atools.ML end *******";
     1.7 -
     1.8 -calclist':= overwritel (!calclist', 
     1.9 -   [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
    1.10 -    ("some_occur_in",
    1.11 -     ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
    1.12 -    ("is_atom"  ,("Atools.is'_atom",eval_is_atom "#is_atom_")),
    1.13 -    ("is_even"  ,("Atools.is'_even",eval_is_even "#is_even_")),
    1.14 -    ("is_const" ,("Atools.is'_const",eval_const "#is_const_")),
    1.15 -    ("le"       ,("Orderings.ord_class.less"        ,eval_equ "#less_")),
    1.16 -    ("leq"      ,("Orderings.ord_class.less_eq"       ,eval_equ "#less_equal_")),
    1.17 -    ("ident"    ,("Atools.ident",eval_ident "#ident_")),
    1.18 -    ("equal"    ,("HOL.eq",eval_equal "#equal_")),
    1.19 -    ("PLUS"     ,("Groups.plus_class.plus"        ,eval_binop "#add_")),
    1.20 -    ("MINUS"    ,("Groups.minus_class.minus",eval_binop "#sub_")),
    1.21 -    ("TIMES"    ,("Groups.times_class.times"        ,eval_binop "#mult_")),
    1.22 -    ("DIVIDE"  ,("Fields.inverse_class.divide"  ,eval_cancel "#divide_e")),
    1.23 -    ("POWER"   ,("Atools.pow"  ,eval_binop "#power_")),
    1.24 -    ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
    1.25 -    ]);
    1.26  *}
    1.27  setup {* KEStore_Elems.add_calcs
    1.28    [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),