1.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Sat Jun 12 18:33:15 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Tue Jun 15 22:24:20 2021 +0200
     1.3 @@ -34,15 +34,12 @@
     1.4          Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Vereinfache t_t", []))]\<close>
     1.5  
     1.6  (** methods **)
     1.7 -setup \<open>KEStore_Elems.add_mets
     1.8 -    [MethodC.prep_input @{theory} "met_tsimp" [] MethodC.id_empty
     1.9 -	    (["simplification"],
    1.10 -	      [("#Given" ,["Term t_t"]),
    1.11 -		      ("#Find"  ,["normalform n_n"])],
    1.12 -		    {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Rule_Set.empty,
    1.13 -		      errpats = [], nrls = Rule_Set.empty},
    1.14 -	      @{thm refl})]
    1.15 -\<close>
    1.16 +
    1.17 +method met_tsimp : "simplification" =
    1.18 +  \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Rule_Set.empty,
    1.19 +    errpats = [], nrls = Rule_Set.empty}\<close>
    1.20 +  Given: "Term t_t"
    1.21 +  Find: "normalform n_n"
    1.22  
    1.23  ML \<open>
    1.24