1.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Mon Jan 27 21:58:57 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Mon Jan 27 22:26:51 2014 +0100
     1.3 @@ -26,28 +26,8 @@
     1.4  
     1.5  ML {*
     1.6  val thy = @{theory};
     1.7 -
     1.8 +*}
     1.9  (** problems **)
    1.10 -store_pbt
    1.11 - (prep_pbt thy "pbl_simp" [] e_pblID
    1.12 - (["simplification"],
    1.13 -  [("#Given" ,["Term t_t"]),
    1.14 -   ("#Find"  ,["normalform n_n"])
    1.15 -  ],
    1.16 -  append_rls "e_rls" e_rls [(*for preds in where_*)], 
    1.17 -  SOME "Simplify t_t", 
    1.18 -  []));
    1.19 -
    1.20 -store_pbt
    1.21 - (prep_pbt thy "pbl_vereinfache" [] e_pblID
    1.22 - (["vereinfachen"],
    1.23 -  [("#Given" ,["Term t_t"]),
    1.24 -   ("#Find"  ,["normalform n_n"])
    1.25 -  ],
    1.26 -  append_rls "e_rls" e_rls [(*for preds in where_*)], 
    1.27 -  SOME "Vereinfache t_t", 
    1.28 -  []));
    1.29 -*}
    1.30  setup {* KEStore_Elems.add_pbts
    1.31    [(prep_pbt thy "pbl_simp" [] e_pblID
    1.32        (["simplification"],