src/Tools/isac/Knowledge/DiophantEq.thy
changeset 55339 cccd24e959ba
parent 52148 aabc6c8e930a
child 55347 6cee13cd9403
     1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Jan 20 16:15:34 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Tue Jan 21 00:27:44 2014 +0100
     1.3 @@ -33,6 +33,14 @@
     1.4  show_ptyps();
     1.5  get_pbt ["diophantine","equation"];
     1.6  *}
     1.7 +setup {* KEStore_Elems.store_pbts
     1.8 +  [(prep_pbt thy "pbl_equ_dio" [] e_pblID
     1.9 +      (["diophantine","equation"],
    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 +        e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}
    1.15  
    1.16  text {*method solving the usecase*}
    1.17  ML {*