1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Thu Sep 26 17:47:10 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Tue Oct 01 10:47:25 2019 +0200
     1.3 @@ -27,11 +27,11 @@
     1.4  
     1.5  partial_function (tailrec) diophant_equation :: "bool => int => bool"
     1.6    where
     1.7 -"diophant_equation e_e v_v =
     1.8 -  (Repeat
     1.9 -      ((Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' False)) @@
    1.10 -       (Try (Calculate ''PLUS'')) @@
    1.11 -       (Try (Calculate ''TIMES''))) e_e)"
    1.12 +"diophant_equation e_e v_v = (
    1.13 +  Repeat (
    1.14 +    (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) @@
    1.15 +    (Try (Calculate ''PLUS'')) @@
    1.16 +    (Try (Calculate ''TIMES''))) e_e)"
    1.17  setup \<open>KEStore_Elems.add_mets
    1.18      [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
    1.19        (["Test","solve_diophant"],