1.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Wed Dec 14 14:20:25 2016 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Sun Dec 18 16:27:41 2016 +0100
1.3 @@ -29,12 +29,12 @@
1.4 *}
1.5 (** problems **)
1.6 setup {* KEStore_Elems.add_pbts
1.7 - [(prep_pbt thy "pbl_simp" [] e_pblID
1.8 + [(Specify.prep_pbt thy "pbl_simp" [] e_pblID
1.9 (["simplification"],
1.10 [("#Given" ,["Term t_t"]),
1.11 ("#Find" ,["normalform n_n"])],
1.12 append_rls "e_rls" e_rls [(*for preds in where_*)], SOME "Simplify t_t", [])),
1.13 - (prep_pbt thy "pbl_vereinfache" [] e_pblID
1.14 + (Specify.prep_pbt thy "pbl_vereinfache" [] e_pblID
1.15 (["vereinfachen"],
1.16 [("#Given", ["Term t_t"]),
1.17 ("#Find", ["normalform n_n"])],
1.18 @@ -42,7 +42,7 @@
1.19
1.20 (** methods **)
1.21 setup {* KEStore_Elems.add_mets
1.22 - [prep_met thy "met_tsimp" [] e_metID
1.23 + [Specify.prep_met thy "met_tsimp" [] e_metID
1.24 (["simplification"],
1.25 [("#Given" ,["Term t_t"]),
1.26 ("#Find" ,["normalform n_n"])],