1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Thu Mar 15 10:17:44 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Thu Mar 15 12:42:04 2018 +0100
     1.3 @@ -20,23 +20,23 @@
     1.4  
     1.5  text {*problemclass for the usecase*}
     1.6  setup {* KEStore_Elems.add_pbts
     1.7 -  [(Specify.prep_pbt thy "pbl_equ_dio" [] e_pblID
     1.8 +  [(Specify.prep_pbt thy "pbl_equ_dio" [] Celem.e_pblID
     1.9        (["diophantine","equation"],
    1.10          [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    1.11            (*                                      TODO: drop ^^^^^*)
    1.12            ("#Where" ,[]),
    1.13            ("#Find"  ,["boolTestFind s_s"])],
    1.14 -        e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}
    1.15 +        Celem.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}
    1.16  
    1.17  text {*method solving the usecase*}
    1.18  setup {* KEStore_Elems.add_mets
    1.19 -  [Specify.prep_met thy "met_test_diophant" [] e_metID
    1.20 -      (["Test","solve_diophant"]:metID,
    1.21 +  [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
    1.22 +      (["Test","solve_diophant"],
    1.23          [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    1.24            (*                                      TODO: drop ^^^^^*)
    1.25            ("#Where" ,[]),
    1.26            ("#Find"  ,["boolTestFind s_s"])],
    1.27 -        {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls, prls = e_rls, calc = [],
    1.28 +        {rew_ord' = "xxxe_rew_ordxxx", rls' = tval_rls, srls = Celem.e_rls, prls = Celem.e_rls, calc = [],
    1.29            crls = tval_rls, errpats = [], nrls = Test_simplify},
    1.30          "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^
    1.31            "(Repeat                                                          " ^