1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Tue May 28 16:52:30 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Wed May 29 10:36:16 2019 +0200
     1.3 @@ -29,7 +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 +
     1.9  partial_function (tailrec) diophant_equation :: "bool => int => bool"
    1.10    where
    1.11  "diophant_equation e_e v_v =
    1.12 @@ -37,7 +37,6 @@
    1.13        ((Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' False)) @@
    1.14         (Try (Calculate ''PLUS'')) @@
    1.15         (Try (Calculate ''TIMES''))) e_e)"
    1.16 -*)
    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"],
    1.20 @@ -47,11 +46,12 @@
    1.21            ("#Find"  ,["boolTestFind s_s"])],
    1.22          {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [],
    1.23            crls = tval_rls, errpats = [], nrls = Test_simplify},
    1.24 -        "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^
    1.25 +        @{thm diophant_equation.simps}
    1.26 +	    (*"Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^
    1.27            "(Repeat                                                          " ^
    1.28            "    ((Try (Rewrite_Inst [(''bdv'',v_v::int)] ''int_isolate_add'' False)) @@" ^
    1.29            "     (Try (Calculate ''PLUS'')) @@  " ^
    1.30 -          "     (Try (Calculate ''TIMES''))) e_e::bool)")]
    1.31 +          "     (Try (Calculate ''TIMES''))) e_e::bool)"*))]
    1.32  \<close>
    1.33  
    1.34  end
    1.35 \ No newline at end of file