1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Sun Jun 20 12:45:03 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Sun Jun 20 16:26:18 2021 +0200
     1.3 @@ -12,14 +12,15 @@
     1.4    int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
     1.5  
     1.6  text \<open>problemclass for the usecase\<close>
     1.7 -setup \<open>KEStore_Elems.add_pbts
     1.8 -  [(Problem.prep_input @{theory} "pbl_equ_dio" [] Problem.id_empty
     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 -        Rule_Set.empty, SOME "solve (e_e::bool, v_v::int)", [["LinEq", "solve_lineq_equation"]]))]\<close>
    1.15 +
    1.16 +problem pbl_equ_dio : "diophantine/equation" =
    1.17 +  \<open>Rule_Set.empty\<close>
    1.18 +  Method: "LinEq/solve_lineq_equation"
    1.19 +  CAS: "solve (e_e::bool, v_v::int)"
    1.20 +  Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
    1.21 +  (*                                TODO: drop ^^^^^*)
    1.22 +  Where:
    1.23 +  Find: "boolTestFind s_s"
    1.24  
    1.25  text \<open>method solving the usecase\<close>
    1.26