1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Sat Jun 12 18:33:15 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Tue Jun 15 22:24:20 2021 +0200
     1.3 @@ -30,17 +30,16 @@
     1.4      (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>
     1.5      (Try (Calculate ''PLUS'')) #>
     1.6      (Try (Calculate ''TIMES''))) e_e)"
     1.7 -setup \<open>KEStore_Elems.add_mets
     1.8 -    [MethodC.prep_input @{theory} "met_test_diophant" [] MethodC.id_empty
     1.9 -      (["Test", "solve_diophant"],
    1.10 -        [("#Given" ,["boolTestGiven e_e", "intTestGiven (v_v::int)"]),
    1.11 -          (*                                      TODO: drop ^^^^^*)
    1.12 -          ("#Where" ,[]),
    1.13 -          ("#Find"  ,["boolTestFind s_s"])],
    1.14 -        {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
    1.15 -          crls = tval_rls, errpats = [], nrls = Test_simplify},
    1.16 -        @{thm diophant_equation.simps})]
    1.17 -\<close> ML \<open>
    1.18 +
    1.19 +method met_test_diophant : "Test/solve_diophant" =
    1.20 +  \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
    1.21 +    crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
    1.22 +  Program: diophant_equation.simps
    1.23 +  Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
    1.24 +(*                                  TODO: drop ^^^^^*)
    1.25 +  Where:
    1.26 +  Find: "boolTestFind s_s"
    1.27 +ML \<open>
    1.28  \<close> ML \<open>
    1.29  \<close>
    1.30