src/Tools/isac/Knowledge/DiophantEq.thy
changeset 60586 007ef64dbb08
parent 60509 2e0b7ca391dc
child 60587 8af797c555a8
equal deleted inserted replaced
60585:b7071d1dd263 60586:007ef64dbb08
    31     (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>
    31     (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>
    32     (Try (Calculate ''PLUS'')) #>
    32     (Try (Calculate ''PLUS'')) #>
    33     (Try (Calculate ''TIMES''))) e_e)"
    33     (Try (Calculate ''TIMES''))) e_e)"
    34 
    34 
    35 method met_test_diophant : "Test/solve_diophant" =
    35 method met_test_diophant : "Test/solve_diophant" =
    36   \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
    36   \<open>{rew_ord = "Rewrite_Ord.id_empty", rls' = tval_rls, prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, calc = [],
    37     crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
    37     crls = tval_rls, errpats = [], rew_rls = Test_simplify}\<close>
    38   Program: diophant_equation.simps
    38   Program: diophant_equation.simps
    39   Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
    39   Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
    40 (*                                  TODO: drop ^^^^^*)
    40 (*                                  TODO: drop ^^^^^*)
    41   Where:
    41   Where:
    42   Find: "boolTestFind s_s"
    42   Find: "boolTestFind s_s"