src/Tools/isac/Knowledge/DiophantEq.thy
changeset 59898 68883c046963
parent 59852 ea7e6679080e
child 59903 5037ca1b112b
     1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Tue Apr 21 12:26:08 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Tue Apr 21 15:42:50 2020 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  text \<open>problemclass for the usecase\<close>
     1.6  setup \<open>KEStore_Elems.add_pbts
     1.7 -  [(Specify.prep_pbt thy "pbl_equ_dio" [] Celem.e_pblID
     1.8 +  [(Specify.prep_pbt thy "pbl_equ_dio" [] Spec.e_pblID
     1.9        (["diophantine","equation"],
    1.10          [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    1.11            (*                                      TODO: drop ^^^^^*)
    1.12 @@ -33,7 +33,7 @@
    1.13      (Try (Calculate ''PLUS'')) #>
    1.14      (Try (Calculate ''TIMES''))) e_e)"
    1.15  setup \<open>KEStore_Elems.add_mets
    1.16 -    [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
    1.17 +    [Specify.prep_met thy "met_test_diophant" [] Spec.e_metID
    1.18        (["Test","solve_diophant"],
    1.19          [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    1.20            (*                                      TODO: drop ^^^^^*)