1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Tue Feb 19 19:35:12 2019 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Thu Feb 28 12:14:32 2019 +0100
     1.3 @@ -29,6 +29,7 @@
     1.4          Rule.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))]\<close>
     1.5  
     1.6  text \<open>method solving the usecase\<close>
     1.7 +(*ok
     1.8  partial_function (tailrec) diophant_equation :: "bool => int => bool"
     1.9    where
    1.10  "diophant_equation e_e v_v =
    1.11 @@ -36,6 +37,7 @@
    1.12        ((Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' False)) @@
    1.13         (Try (Calculate ''PLUS'')) @@
    1.14         (Try (Calculate ''TIMES''))) e_e)"
    1.15 +*)
    1.16  setup \<open>KEStore_Elems.add_mets
    1.17      [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
    1.18        (["Test","solve_diophant"],