1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Fri Jan 31 17:50:50 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Sat Feb 01 16:44:45 2014 +0100
     1.3 @@ -47,5 +47,20 @@
     1.4   "     (Try (Calculate TIMES))) e_e::bool)"
     1.5   ))
     1.6  *}
     1.7 +setup {* KEStore_Elems.add_mets
     1.8 +  [prep_met thy "met_test_diophant" [] e_metID
     1.9 +      (["Test","solve_diophant"]:metID,
    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 +        {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls, prls = e_rls, calc = [],
    1.15 +          crls = tval_rls, errpats = [], nrls = Test_simplify},
    1.16 +        "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^
    1.17 +          "(Repeat                                                          " ^
    1.18 +          "    ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
    1.19 +          "     (Try (Calculate PLUS)) @@  " ^
    1.20 +          "     (Try (Calculate TIMES))) e_e::bool)")]
    1.21 +*}
    1.22  
    1.23  end
    1.24 \ No newline at end of file