1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Tue May 19 12:33:35 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Wed May 20 12:52:09 2020 +0200
     1.3 @@ -16,12 +16,12 @@
     1.4  text \<open>problemclass for the usecase\<close>
     1.5  setup \<open>KEStore_Elems.add_pbts
     1.6    [(Problem.prep_input thy "pbl_equ_dio" [] Problem.id_empty
     1.7 -      (["diophantine","equation"],
     1.8 -        [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
     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 +        Rule_Set.empty, SOME "solve (e_e::bool, v_v::int)", [["LinEq", "solve_lineq_equation"]]))]\<close>
    1.16  
    1.17  text \<open>method solving the usecase\<close>
    1.18  
    1.19 @@ -34,8 +34,8 @@
    1.20      (Try (Calculate ''TIMES''))) e_e)"
    1.21  setup \<open>KEStore_Elems.add_mets
    1.22      [Method.prep_input thy "met_test_diophant" [] Method.id_empty
    1.23 -      (["Test","solve_diophant"],
    1.24 -        [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    1.25 +      (["Test", "solve_diophant"],
    1.26 +        [("#Given" ,["boolTestGiven e_e", "intTestGiven (v_v::int)"]),
    1.27            (*                                      TODO: drop ^^^^^*)
    1.28            ("#Where" ,[]),
    1.29            ("#Find"  ,["boolTestFind s_s"])],