src/Tools/isac/Knowledge/Simplify.thy
changeset 59269 1da53d1540fe
parent 59186 d9c3e373f8f5
child 59279 255c853ea2f0
     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"])],