1.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Thu Mar 15 10:17:44 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Thu Mar 15 12:42:04 2018 +0100
     1.3 @@ -29,25 +29,25 @@
     1.4  *}
     1.5  (** problems **)
     1.6  setup {* KEStore_Elems.add_pbts
     1.7 -  [(Specify.prep_pbt thy "pbl_simp" [] e_pblID
     1.8 +  [(Specify.prep_pbt thy "pbl_simp" [] Celem.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 -    (Specify.prep_pbt thy "pbl_vereinfache" [] e_pblID
    1.14 +        Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], SOME "Simplify t_t", [])),
    1.15 +    (Specify.prep_pbt thy "pbl_vereinfache" [] Celem.e_pblID
    1.16        (["vereinfachen"],
    1.17          [("#Given", ["Term t_t"]),
    1.18            ("#Find", ["normalform n_n"])],
    1.19 -        append_rls "e_rls" e_rls [(*for preds in where_*)], SOME "Vereinfache t_t", []))] *}
    1.20 +        Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], SOME "Vereinfache t_t", []))] *}
    1.21  
    1.22  (** methods **)
    1.23  setup {* KEStore_Elems.add_mets
    1.24 -  [Specify.prep_met thy "met_tsimp" [] e_metID
    1.25 +  [Specify.prep_met thy "met_tsimp" [] Celem.e_metID
    1.26  	    (["simplification"],
    1.27  	      [("#Given" ,["Term t_t"]),
    1.28  		      ("#Find"  ,["normalform n_n"])],
    1.29 -		    {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls=e_rls, crls = e_rls,
    1.30 -		      errpats = [], nrls = e_rls},
    1.31 +		    {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls, crls = Celem.e_rls,
    1.32 +		      errpats = [], nrls = Celem.e_rls},
    1.33  	      "empty_script")]
    1.34  *}
    1.35