1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Sun Feb 02 02:45:11 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Sun Feb 02 03:09:40 2014 +0100
     1.3 @@ -29,24 +29,6 @@
     1.4          e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}
     1.5  
     1.6  text {*method solving the usecase*}
     1.7 -ML {*
     1.8 -store_met
     1.9 -(prep_met thy "met_test_diophant" [] e_metID
    1.10 - (["Test","solve_diophant"]:metID,
    1.11 -  [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    1.12 -  (*                                      TODO: drop ^^^^^*)
    1.13 -   ("#Where" ,[]),
    1.14 -   ("#Find"  ,["boolTestFind s_s"]) 
    1.15 -  ],
    1.16 -   {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
    1.17 -    prls = e_rls, calc = [], crls = tval_rls, errpats = [], nrls = Test_simplify},
    1.18 - "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^
    1.19 - "(Repeat                                                          " ^
    1.20 - "    ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
    1.21 - "     (Try (Calculate PLUS)) @@  " ^
    1.22 - "     (Try (Calculate TIMES))) e_e::bool)"
    1.23 - ))
    1.24 -*}
    1.25  setup {* KEStore_Elems.add_mets
    1.26    [prep_met thy "met_test_diophant" [] e_metID
    1.27        (["Test","solve_diophant"]:metID,