1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Wed Sep 05 18:09:56 2018 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Wed Nov 21 12:32:54 2018 +0100
     1.3 @@ -16,20 +16,20 @@
     1.4  axiomatization where
     1.5    int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
     1.6  
     1.7 -ML {*val thy = @{theory}*}
     1.8 +ML \<open>val thy = @{theory}\<close>
     1.9  
    1.10 -text {*problemclass for the usecase*}
    1.11 -setup {* KEStore_Elems.add_pbts
    1.12 +text \<open>problemclass for the usecase\<close>
    1.13 +setup \<open>KEStore_Elems.add_pbts
    1.14    [(Specify.prep_pbt thy "pbl_equ_dio" [] Celem.e_pblID
    1.15        (["diophantine","equation"],
    1.16          [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    1.17            (*                                      TODO: drop ^^^^^*)
    1.18            ("#Where" ,[]),
    1.19            ("#Find"  ,["boolTestFind s_s"])],
    1.20 -        Rule.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}
    1.21 +        Rule.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))]\<close>
    1.22  
    1.23 -text {*method solving the usecase*}
    1.24 -setup {* KEStore_Elems.add_mets
    1.25 +text \<open>method solving the usecase\<close>
    1.26 +setup \<open>KEStore_Elems.add_mets
    1.27    [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
    1.28        (["Test","solve_diophant"],
    1.29          [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    1.30 @@ -43,6 +43,6 @@
    1.31            "    ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
    1.32            "     (Try (Calculate PLUS)) @@  " ^
    1.33            "     (Try (Calculate TIMES))) e_e::bool)")]
    1.34 -*}
    1.35 +\<close>
    1.36  
    1.37  end
    1.38 \ No newline at end of file