src/Tools/isac/Knowledge/DiophantEq.thy
changeset 60154 2ab0d1523731
parent 59997 46fe5a8c3911
child 60278 343efa173023
equal deleted inserted replaced
60153:fa8d902b60bc 60154:2ab0d1523731
    31   Repeat (
    31   Repeat (
    32     (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>
    32     (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>
    33     (Try (Calculate ''PLUS'')) #>
    33     (Try (Calculate ''PLUS'')) #>
    34     (Try (Calculate ''TIMES''))) e_e)"
    34     (Try (Calculate ''TIMES''))) e_e)"
    35 setup \<open>KEStore_Elems.add_mets
    35 setup \<open>KEStore_Elems.add_mets
    36     [Method.prep_input thy "met_test_diophant" [] Method.id_empty
    36     [MethodC.prep_input thy "met_test_diophant" [] MethodC.id_empty
    37       (["Test", "solve_diophant"],
    37       (["Test", "solve_diophant"],
    38         [("#Given" ,["boolTestGiven e_e", "intTestGiven (v_v::int)"]),
    38         [("#Given" ,["boolTestGiven e_e", "intTestGiven (v_v::int)"]),
    39           (*                                      TODO: drop ^^^^^*)
    39           (*                                      TODO: drop ^^^^^*)
    40           ("#Where" ,[]),
    40           ("#Where" ,[]),
    41           ("#Find"  ,["boolTestFind s_s"])],
    41           ("#Find"  ,["boolTestFind s_s"])],