1.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Sun Feb 02 02:45:11 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Sun Feb 02 03:09:40 2014 +0100
     1.3 @@ -42,20 +42,8 @@
     1.4  ML {*
     1.5  @{thm mult_commute}
     1.6  *}
     1.7 -ML {*
     1.8  
     1.9  (** methods **)
    1.10 -
    1.11 -store_met
    1.12 - (prep_met thy "met_tsimp" [] e_metID
    1.13 -	   (["simplification"],
    1.14 -	    [("#Given" ,["Term t_t"]),
    1.15 -		     ("#Find"  ,["normalform n_n"])],
    1.16 -	    {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls=e_rls,
    1.17 -	     crls = e_rls, errpats = [], nrls = e_rls},
    1.18 -	     "empty_script"));
    1.19 -*}
    1.20 -(** methods **)
    1.21  setup {* KEStore_Elems.add_mets
    1.22    [prep_met thy "met_tsimp" [] e_metID
    1.23  	    (["simplification"],