src/Tools/isac/Knowledge/DiophantEq.thy
changeset 59269 1da53d1540fe
parent 55380 7be2ad0e4acb
child 59406 509d70b507e5
     1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Wed Dec 14 14:20:25 2016 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Sun Dec 18 16:27:41 2016 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  text {*problemclass for the usecase*}
     1.6  setup {* KEStore_Elems.add_pbts
     1.7 -  [(prep_pbt thy "pbl_equ_dio" [] e_pblID
     1.8 +  [(Specify.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 @@ -30,7 +30,7 @@
    1.13  
    1.14  text {*method solving the usecase*}
    1.15  setup {* KEStore_Elems.add_mets
    1.16 -  [prep_met thy "met_test_diophant" [] e_metID
    1.17 +  [Specify.prep_met thy "met_test_diophant" [] e_metID
    1.18        (["Test","solve_diophant"]:metID,
    1.19          [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    1.20            (*                                      TODO: drop ^^^^^*)