1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Wed Sep 05 18:09:56 2018 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Wed Nov 21 12:32:54 2018 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  theory Equation imports Base_Tools begin
     1.6  
     1.7 -text {* univariate equations over terms :
     1.8 +text \<open>univariate equations over terms :
     1.9    In 2003 Richard Lang prototyped ISAC's equation solver while also alpha-testing
    1.10    the Lucas-Interpreter's Subproblem mechanism.
    1.11    This prototype suffers from the drop-out of Matthias Goldgruber for a year,
    1.12 @@ -13,7 +13,7 @@
    1.13    replaced simplifiers by many specific theorems for specific terms in specific
    1.14    phases of equation solving; these specific solutions wait for generalisation
    1.15    in future improvements of ISAC's equation solver.
    1.16 -*}
    1.17 +\<close>
    1.18  
    1.19  consts
    1.20  
    1.21 @@ -29,25 +29,25 @@
    1.22  					 => bool"
    1.23                    ("((Script Function2Equality (_ _ =))// (_))" 9)
    1.24  
    1.25 -text {* defines equation and univariate-equation
    1.26 +text \<open>defines equation and univariate-equation
    1.27          created by: rlang 
    1.28                date: 02.09
    1.29          changed by: rlang
    1.30          last change by: rlang
    1.31                    date: 02.11.29
    1.32 -        (c) by Richard Lang, 2003 *}
    1.33 +        (c) by Richard Lang, 2003\<close>
    1.34  
    1.35 -ML {*
    1.36 +ML \<open>
    1.37  val thy = @{theory};
    1.38  val ctxt = Rule.thy2ctxt thy;
    1.39  
    1.40  val univariate_equation_prls = 
    1.41      Rule.append_rls "univariate_equation_prls" Rule.e_rls 
    1.42  	       [Rule.Calc ("Tools.matches",eval_matches "")];
    1.43 -*}
    1.44 -setup {* KEStore_Elems.add_rlss [("univariate_equation_prls",
    1.45 -  (Context.theory_name @{theory}, LTool.prep_rls @{theory} univariate_equation_prls))] *}
    1.46 -setup {* KEStore_Elems.add_pbts
    1.47 +\<close>
    1.48 +setup \<open>KEStore_Elems.add_rlss [("univariate_equation_prls",
    1.49 +  (Context.theory_name @{theory}, LTool.prep_rls @{theory} univariate_equation_prls))]\<close>
    1.50 +setup \<open>KEStore_Elems.add_pbts
    1.51    [(Specify.prep_pbt thy "pbl_equ" [] Celem.e_pblID
    1.52        (["equation"],
    1.53          [("#Given" ,["equality e_e","solveFor v_v"]),
    1.54 @@ -60,10 +60,10 @@
    1.55          [("#Given" ,["equality e_e","solveFor v_v"]),
    1.56            ("#Where" ,["matches (?a = ?b) e_e"]),
    1.57            ("#Find"  ,["solutions v_v'i'"])],
    1.58 -        univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))] *}
    1.59 +        univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))]\<close>
    1.60  
    1.61  
    1.62 -ML{*
    1.63 +ML\<open>
    1.64  (*.function for handling the cas-input "solve (x+1=2, x)":
    1.65     make a model which is already in ctree-internal format.*)
    1.66  (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
    1.67 @@ -77,20 +77,20 @@
    1.68        [(the o (TermC.parseNEW ctxt)) "L"])
    1.69       ]
    1.70    | argl2dtss _ = error "Equation.ML: wrong argument for argl2dtss";
    1.71 -*}
    1.72 -setup {* KEStore_Elems.add_cas
    1.73 +\<close>
    1.74 +setup \<open>KEStore_Elems.add_cas
    1.75    [((Thm.term_of o the o (TermC.parse thy)) "solveTest", 
    1.76        (("Test", ["univariate","equation","test"], ["no_met"]), argl2dtss)),
    1.77      ((Thm.term_of o the o (TermC.parse thy)) "solve",
    1.78 -      (("Isac", ["univariate","equation"], ["no_met"]), argl2dtss))]*}
    1.79 +      (("Isac", ["univariate","equation"], ["no_met"]), argl2dtss))]\<close>
    1.80  
    1.81  
    1.82 -setup {* KEStore_Elems.add_mets
    1.83 +setup \<open>KEStore_Elems.add_mets
    1.84    [Specify.prep_met thy "met_equ" [] Celem.e_metID
    1.85  	    (["Equation"], [],
    1.86  	      {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
    1.87            errpats = [], nrls = Rule.e_rls},
    1.88          "empty_script")]
    1.89 -*}
    1.90 +\<close>
    1.91  
    1.92  end
    1.93 \ No newline at end of file