diff -r 3f58f3a2c3e6 -r 546bd1b027cc src/Tools/isac/Knowledge/DiophantEq.thy
--- a/src/Tools/isac/Knowledge/DiophantEq.thy	Fri Feb 15 16:52:05 2019 +0100
+++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Tue Feb 19 19:35:12 2019 +0100
@@ -29,6 +29,13 @@
         Rule.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))]\<close>
 
 text \<open>method solving the usecase\<close>
+partial_function (tailrec) diophant_equation :: "bool => int => bool"
+  where
+"diophant_equation e_e v_v =
+  (Repeat
+      ((Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' False)) @@
+       (Try (Calculate ''PLUS'')) @@
+       (Try (Calculate ''TIMES''))) e_e)"
 setup \<open>KEStore_Elems.add_mets
     [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
       (["Test","solve_diophant"],