1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Sep 05 18:09:56 2018 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed Nov 21 12:32:54 2018 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4  *)
     1.5    integral_pow:      "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
     1.6  
     1.7 -ML {*
     1.8 +ML \<open>
     1.9  val thy = @{theory};
    1.10  
    1.11  (** eval functions **)
    1.12 @@ -107,11 +107,11 @@
    1.13      else SOME ((Rule.term2str p) ^ " = False",
    1.14  	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.15    | eval_is_f_x _ _ _ _ = NONE;
    1.16 -*}
    1.17 -setup {* KEStore_Elems.add_calcs
    1.18 +\<close>
    1.19 +setup \<open>KEStore_Elems.add_calcs
    1.20    [("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
    1.21 -    ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))] *}
    1.22 -ML {*
    1.23 +    ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))]\<close>
    1.24 +ML \<open>
    1.25  (** rulesets **)
    1.26  
    1.27  (*.rulesets for integration.*)
    1.28 @@ -140,8 +140,8 @@
    1.29  		  Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
    1.30  		  ],
    1.31  	 scr = Rule.EmptyScr};
    1.32 -*}
    1.33 -ML {*
    1.34 +\<close>
    1.35 +ML \<open>
    1.36  val add_new_c = 
    1.37      Rule.Seq {id="add_new_c", preconds = [], 
    1.38  	 rew_ord = ("termlessI",termlessI), 
    1.39 @@ -162,8 +162,8 @@
    1.40  		   Rule.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
    1.41  		   ],
    1.42  	 scr = Rule.EmptyScr};
    1.43 -*}
    1.44 -ML {*
    1.45 +\<close>
    1.46 +ML \<open>
    1.47  
    1.48  (*.rulesets for simplifying Integrals.*)
    1.49  
    1.50 @@ -323,8 +323,8 @@
    1.51  	 scr = Rule.EmptyScr};
    1.52  
    1.53  val prep_rls' = LTool.prep_rls @{theory};
    1.54 -*}
    1.55 -setup {* KEStore_Elems.add_rlss 
    1.56 +\<close>
    1.57 +setup \<open>KEStore_Elems.add_rlss 
    1.58    [("integration_rules", (Context.theory_name @{theory}, prep_rls' integration_rules)), 
    1.59    ("add_new_c", (Context.theory_name @{theory}, prep_rls' add_new_c)), 
    1.60    ("simplify_Integral", (Context.theory_name @{theory}, prep_rls' simplify_Integral)), 
    1.61 @@ -334,10 +334,10 @@
    1.62    ("norm_Rational_noadd_fractions", (Context.theory_name @{theory},
    1.63      prep_rls' norm_Rational_noadd_fractions)), 
    1.64    ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory},
    1.65 -    prep_rls' norm_Rational_rls_noadd_fractions))] *}
    1.66 +    prep_rls' norm_Rational_rls_noadd_fractions))]\<close>
    1.67  
    1.68  (** problems **)
    1.69 -setup {* KEStore_Elems.add_pbts
    1.70 +setup \<open>KEStore_Elems.add_pbts
    1.71    [(Specify.prep_pbt thy "pbl_fun_integ" [] Celem.e_pblID
    1.72        (["integrate","function"],
    1.73          [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.74 @@ -352,10 +352,10 @@
    1.75            ("#Find"  ,["antiDerivativeName F_F"])],
    1.76          Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], 
    1.77          SOME "Integrate (f_f, v_v)", 
    1.78 -        [["diff","integration","named"]]))] *}
    1.79 +        [["diff","integration","named"]]))]\<close>
    1.80  
    1.81  (** methods **)
    1.82 -setup {* KEStore_Elems.add_mets
    1.83 +setup \<open>KEStore_Elems.add_mets
    1.84    [Specify.prep_met thy "met_diffint" [] Celem.e_metID
    1.85  	    (["diff","integration"],
    1.86  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find"  ,["antiDerivative F_F"])],
    1.87 @@ -374,6 +374,6 @@
    1.88            "  (let t_t = Take (F_F v_v = Integral f_f D v_v)                            " ^
    1.89            "   in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@  " ^
    1.90            "       (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_t)            ")]
    1.91 -*}
    1.92 +\<close>
    1.93  
    1.94  end
    1.95 \ No newline at end of file