src/Tools/isac/Knowledge/DiophantEq.thy
changeset 55363 d78bc1342183
parent 55359 73dc85c025ab
child 55373 4f3f530f3cf6
     1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Jan 27 21:58:57 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Jan 27 22:26:51 2014 +0100
     1.3 @@ -19,18 +19,6 @@
     1.4  ML {*val thy = @{theory}*}
     1.5  
     1.6  text {*problemclass for the usecase*}
     1.7 -ML {*
     1.8 -store_pbt
     1.9 - (prep_pbt thy "pbl_equ_dio" [] e_pblID
    1.10 - (["diophantine","equation"],
    1.11 -  [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    1.12 -  (*                                      TODO: drop ^^^^^*)
    1.13 -   ("#Where" ,[]),
    1.14 -   ("#Find"  ,["boolTestFind s_s"]) 
    1.15 -  ],
    1.16 -  e_rls, SOME "solve (e_e::bool, v_v::int)",
    1.17 -  [["LinEq","solve_lineq_equation"]])); (*-----TODO*)
    1.18 -*}
    1.19  setup {* KEStore_Elems.add_pbts
    1.20    [(prep_pbt thy "pbl_equ_dio" [] e_pblID
    1.21        (["diophantine","equation"],