1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Fri Feb 15 16:52:05 2019 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Tue Feb 19 19:35:12 2019 +0100
     1.3 @@ -29,6 +29,13 @@
     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 +partial_function (tailrec) diophant_equation :: "bool => int => bool"
     1.8 +  where
     1.9 +"diophant_equation e_e v_v =
    1.10 +  (Repeat
    1.11 +      ((Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' False)) @@
    1.12 +       (Try (Calculate ''PLUS'')) @@
    1.13 +       (Try (Calculate ''TIMES''))) e_e)"
    1.14  setup \<open>KEStore_Elems.add_mets
    1.15      [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
    1.16        (["Test","solve_diophant"],