3 000516 |
3 000516 |
4 *) |
4 *) |
5 |
5 |
6 theory Diff imports Calculus Trig LogExp Rational Root Poly Atools begin |
6 theory Diff imports Calculus Trig LogExp Rational Root Poly Atools begin |
7 |
7 |
|
8 ML {* |
|
9 @{term "sin x"} |
|
10 *} |
|
11 |
8 consts |
12 consts |
9 |
13 |
10 d_d :: "[real, real]=> real" |
14 d_d :: "[real, real]=> real" |
11 sin, cos :: "real => real" |
15 (*sin, cos :: "real => real" already in Isabelle2009-2*) |
12 (* |
16 (* |
13 log, ln :: "real => real" |
17 log, ln :: "real => real" |
14 nlog :: "[real, real] => real" |
18 nlog :: "[real, real] => real" |
15 exp :: "real => real" ("E'_ ^^^ _" 80) |
19 exp :: "real => real" ("E'_ ^^^ _" 80) |
16 *) |
20 *) |
17 (*descriptions in the related problems*) |
21 (*descriptions in the related problems*) |
18 derivativeEq :: bool => una |
22 derivativeEq :: "bool => una" |
19 |
23 |
20 (*predicates*) |
24 (*predicates*) |
21 primed :: "'a => 'a" (*"primed A" -> "A'"*) |
25 primed :: "'a => 'a" (*"primed A" -> "A'"*) |
22 |
26 |
23 (*the CAS-commands, eg. "Diff (2*x^^^3, x)", |
27 (*the CAS-commands, eg. "Diff (2*x^^^3, x)", |
28 (*subproblem and script-name*) |
32 (*subproblem and script-name*) |
29 differentiate :: "[ID * (ID list) * ID, real,real] => real" |
33 differentiate :: "[ID * (ID list) * ID, real,real] => real" |
30 ("(differentiate (_)/ (_ _ ))" 9) |
34 ("(differentiate (_)/ (_ _ ))" 9) |
31 DiffScr :: "[real,real, real] => real" |
35 DiffScr :: "[real,real, real] => real" |
32 ("((Script DiffScr (_ _ =))// (_))" 9) |
36 ("((Script DiffScr (_ _ =))// (_))" 9) |
33 DiffEqScr :: "[bool,real, bool] => bool" |
37 DiffEqScr :: "[bool,real, bool] => bool" |
34 ("((Script DiffEqScr (_ _ =))// (_))" 9) |
38 ("((Script DiffEqScr (_ _ =))// (_))" 9) |
35 |
39 |
36 text {*a variant of the derivatives defintion: |
40 text {*a variant of the derivatives defintion: |
37 |
41 |
38 d_d :: "(real => real) => (real => real)" |
42 d_d :: "(real => real) => (real => real)" |
120 [Calc ("Atools.occurs'_in", eval_occurs_in ""), |
124 [Calc ("Atools.occurs'_in", eval_occurs_in ""), |
121 Thm ("not_true",num_str @{thm not_true}), |
125 Thm ("not_true",num_str @{thm not_true}), |
122 Thm ("not_false",num_str @{thm not_false}), |
126 Thm ("not_false",num_str @{thm not_false}), |
123 Calc ("op <",eval_equ "#less_"), |
127 Calc ("op <",eval_equ "#less_"), |
124 Thm ("and_true",num_str @{thm and_true}), |
128 Thm ("and_true",num_str @{thm and_true}), |
125 Thm ("and_false",num_str @{thm and_false) |
129 Thm ("and_false",num_str @{thm and_false}) |
126 ], |
130 ], |
127 srls = Erls, calc = [], |
131 srls = Erls, calc = [], |
128 rules = [Thm ("frac_conv", num_str @{thm frac_conv}), |
132 rules = [Thm ("frac_conv", num_str @{thm frac_conv}), |
129 Thm ("sqrt_conv_bdv", num_str @{thm sqrt_conv_bdv}), |
133 Thm ("sqrt_conv_bdv", num_str @{thm sqrt_conv_bdv}), |
130 Thm ("sqrt_conv_bdv_n", num_str @{thm sqrt_conv_bdv_n}), |
134 Thm ("sqrt_conv_bdv_n", num_str @{thm sqrt_conv_bdv_n}), |
136 (*a / b * (c / d) = a * c / (b * d)*) |
140 (*a / b * (c / d) = a * c / (b * d)*) |
137 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
141 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
138 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
142 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
139 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}) |
143 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}) |
140 (*?y / ?z * ?x = ?y * ?x / ?z*) |
144 (*?y / ?z * ?x = ?y * ?x / ?z*) |
141 (* |
|
142 Thm ("", num_str @{}),*) |
|
143 ], |
145 ], |
144 scr = EmptyScr}; |
146 scr = EmptyScr}; |
145 |
147 *} |
|
148 ML {* |
146 (*.beautifies a term after differentiation.*) |
149 (*.beautifies a term after differentiation.*) |
147 val diff_sym_conv = |
150 val diff_sym_conv = |
148 Rls {id="diff_sym_conv", |
151 Rls {id="diff_sym_conv", |
149 preconds = [], |
152 preconds = [], |
150 rew_ord = ("termlessI",termlessI), |
153 rew_ord = ("termlessI",termlessI), |
178 rules = [Calc("Tools.lhs", eval_lhs "eval_lhs_"), |
181 rules = [Calc("Tools.lhs", eval_lhs "eval_lhs_"), |
179 Calc("Tools.rhs", eval_rhs "eval_rhs_"), |
182 Calc("Tools.rhs", eval_rhs "eval_rhs_"), |
180 Calc("Diff.primed", eval_primed "Diff.primed") |
183 Calc("Diff.primed", eval_primed "Diff.primed") |
181 ], |
184 ], |
182 scr = EmptyScr}; |
185 scr = EmptyScr}; |
183 |
186 *} |
|
187 ML {* |
184 (*..*) |
188 (*..*) |
185 val erls_diff = |
189 val erls_diff = |
186 append_rls "erls_differentiate.." e_rls |
190 append_rls "erls_differentiate.." e_rls |
187 [Thm ("not_true",num_str @{thm not_true}), |
191 [Thm ("not_true",num_str @{thm not_true}), |
188 Thm ("not_false",num_str @{thm not_false}), |
192 Thm ("not_false",num_str @{thm not_false}), |
218 *) |
222 *) |
219 Thm ("diff_const",num_str @{thm diff_const}), |
223 Thm ("diff_const",num_str @{thm diff_const}), |
220 Thm ("diff_var",num_str @{thm diff_var}) |
224 Thm ("diff_var",num_str @{thm diff_var}) |
221 ], |
225 ], |
222 scr = EmptyScr}; |
226 scr = EmptyScr}; |
223 |
227 *} |
|
228 ML {* |
224 (*.normalisation for checking user-input.*) |
229 (*.normalisation for checking user-input.*) |
225 val norm_diff = |
230 val norm_diff = |
226 Rls {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI), |
231 Rls {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI), |
227 erls = Erls, srls = Erls, calc = [], |
232 erls = Erls, srls = Erls, calc = [], |
228 rules = [Rls_ diff_rules, |
233 rules = [Rls_ diff_rules, |
235 ("norm_diff", prep_rls norm_diff), |
240 ("norm_diff", prep_rls norm_diff), |
236 ("diff_conv", prep_rls diff_conv), |
241 ("diff_conv", prep_rls diff_conv), |
237 ("diff_sym_conv", prep_rls diff_sym_conv) |
242 ("diff_sym_conv", prep_rls diff_sym_conv) |
238 ]); |
243 ]); |
239 |
244 |
240 |
245 *} |
|
246 ML {* |
241 (** problem types **) |
247 (** problem types **) |
242 |
248 |
243 store_pbt |
249 store_pbt |
244 (prep_pbt thy "pbl_fun" [] e_pblID |
250 (prep_pbt thy "pbl_fun" [] e_pblID |
245 (["function"], [], e_rls, NONE, [])); |
251 (["function"], [], e_rls, NONE, [])); |
246 |
252 |
247 store_pbt |
253 store_pbt |
248 (prep_pbt thy "pbl_fun_deriv" [] e_pblID |
254 (prep_pbt thy "pbl_fun_deriv" [] e_pblID |
249 (["derivative_of","function"], |
255 (["derivative_of","function"], |
250 [("#Given" ,["functionTerm f_","differentiateFor v_v"]), |
256 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), |
251 ("#Find" ,["derivative f_'_"]) |
257 ("#Find" ,["derivative f_f'"]) |
252 ], |
258 ], |
253 append_rls "e_rls" e_rls [], |
259 append_rls "e_rls" e_rls [], |
254 SOME "Diff (f_, v_v)", [["diff","differentiate_on_R"], |
260 SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"], |
255 ["diff","after_simplification"]])); |
261 ["diff","after_simplification"]])); |
256 |
262 |
257 (*here "named" is used differently from Integration"*) |
263 (*here "named" is used differently from Integration"*) |
258 store_pbt |
264 store_pbt |
259 (prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID |
265 (prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID |
260 (["named","derivative_of","function"], |
266 (["named","derivative_of","function"], |
261 [("#Given" ,["functionEq f_","differentiateFor v_v"]), |
267 [("#Given" ,["functionEq f_f","differentiateFor v_v"]), |
262 ("#Find" ,["derivativeEq f_'_"]) |
268 ("#Find" ,["derivativeEq f_f'"]) |
263 ], |
269 ], |
264 append_rls "e_rls" e_rls [], |
270 append_rls "e_rls" e_rls [], |
265 SOME "Differentiate (f_, v_v)", [["diff","differentiate_equality"]])); |
271 SOME "Differentiate (f_f, v_v)", [["diff","differentiate_equality"]])); |
266 |
272 *} |
|
273 ML {* |
267 |
274 |
268 (** methods **) |
275 (** methods **) |
269 |
276 |
270 store_met |
277 store_met |
271 (prep_met thy "met_diff" [] e_metID |
278 (prep_met thy "met_diff" [] e_metID |
274 crls = Atools_erls, nrls = norm_diff}, "empty_script")); |
281 crls = Atools_erls, nrls = norm_diff}, "empty_script")); |
275 |
282 |
276 store_met |
283 store_met |
277 (prep_met thy "met_diff_onR" [] e_metID |
284 (prep_met thy "met_diff_onR" [] e_metID |
278 (["diff","differentiate_on_R"], |
285 (["diff","differentiate_on_R"], |
279 [("#Given" ,["functionTerm f_","differentiateFor v_v"]), |
286 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), |
280 ("#Find" ,["derivative f_'_"]) |
287 ("#Find" ,["derivative f_f'"]) |
281 ], |
288 ], |
282 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, |
289 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, |
283 prls=e_rls, crls = Atools_erls, nrls = norm_diff}, |
290 prls=e_rls, crls = Atools_erls, nrls = norm_diff}, |
284 "Script DiffScr (f_::real) (v_v::real) = " ^ |
291 "Script DiffScr (f_f::real) (v_v::real) = " ^ |
285 " (let f'_ = Take (d_d v_v f_) " ^ |
292 " (let f_f' = Take (d_d v_v f_f) " ^ |
286 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^ |
293 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^ |
287 " (Repeat " ^ |
294 " (Repeat " ^ |
288 " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^ |
295 " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^ |
289 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^ |
296 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^ |
290 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^ |
297 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^ |
300 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^ |
307 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^ |
301 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^ |
308 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^ |
302 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^ |
309 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^ |
303 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^ |
310 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^ |
304 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^ |
311 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^ |
305 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)" |
312 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')" |
306 )); |
313 )); |
307 |
314 *} |
|
315 ML {* |
308 store_met |
316 store_met |
309 (prep_met thy "met_diff_simpl" [] e_metID |
317 (prep_met thy "met_diff_simpl" [] e_metID |
310 (["diff","diff_simpl"], |
318 (["diff","diff_simpl"], |
311 [("#Given" ,["functionTerm f_","differentiateFor v_v"]), |
319 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), |
312 ("#Find" ,["derivative f_'_"]) |
320 ("#Find" ,["derivative f_f'"]) |
313 ], |
321 ], |
314 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, |
322 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, |
315 prls=e_rls, crls = Atools_erls, nrls = norm_diff}, |
323 prls=e_rls, crls = Atools_erls, nrls = norm_diff}, |
316 "Script DiffScr (f_::real) (v_v::real) = " ^ |
324 "Script DiffScr (f_f::real) (v_v::real) = " ^ |
317 " (let f'_ = Take (d_d v_v f_) " ^ |
325 " (let f_f' = Take (d_d v_v f_f) " ^ |
318 " in (( " ^ |
326 " in (( " ^ |
319 " (Repeat " ^ |
327 " (Repeat " ^ |
320 " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^ |
328 " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^ |
321 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^ |
329 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^ |
322 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^ |
330 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^ |
332 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^ |
340 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^ |
333 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^ |
341 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^ |
334 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^ |
342 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^ |
335 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^ |
343 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^ |
336 " (Repeat (Rewrite_Set make_polynomial False)))) " ^ |
344 " (Repeat (Rewrite_Set make_polynomial False)))) " ^ |
337 " )) f'_)" |
345 " )) f_f')" |
338 )); |
346 )); |
339 |
347 |
340 store_met |
348 store_met |
341 (prep_met thy "met_diff_equ" [] e_metID |
349 (prep_met thy "met_diff_equ" [] e_metID |
342 (["diff","differentiate_equality"], |
350 (["diff","differentiate_equality"], |
343 [("#Given" ,["functionEq f_","differentiateFor v_v"]), |
351 [("#Given" ,["functionEq f_f","differentiateFor v_v"]), |
344 ("#Find" ,["derivativeEq f_'_"]) |
352 ("#Find" ,["derivativeEq f_f'"]) |
345 ], |
353 ], |
346 {rew_ord'="tless_true", rls' = erls_diff, calc = [], |
354 {rew_ord'="tless_true", rls' = erls_diff, calc = [], |
347 srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff}, |
355 srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff}, |
348 "Script DiffEqScr (f_::bool) (v_v::real) = " ^ |
356 "Script DiffEqScr (f_f::bool) (v_v::real) = " ^ |
349 " (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) " ^ |
357 " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^ |
350 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^ |
358 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^ |
351 " (Repeat " ^ |
359 " (Repeat " ^ |
352 " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^ |
360 " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^ |
353 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif False)) Or " ^ |
361 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif False)) Or " ^ |
354 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^ |
362 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^ |
365 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^ |
373 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^ |
366 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^ |
374 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^ |
367 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^ |
375 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^ |
368 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^ |
376 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^ |
369 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^ |
377 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^ |
370 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)" |
378 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')" |
371 )); |
379 )); |
372 |
380 |
373 store_met |
381 store_met |
374 (prep_met thy "met_diff_after_simp" [] e_metID |
382 (prep_met thy "met_diff_after_simp" [] e_metID |
375 (["diff","after_simplification"], |
383 (["diff","after_simplification"], |
376 [("#Given" ,["functionTerm f_","differentiateFor v_v"]), |
384 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), |
377 ("#Find" ,["derivative f_'_"]) |
385 ("#Find" ,["derivative f_f'"]) |
378 ], |
386 ], |
379 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls, |
387 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls, |
380 crls=Atools_erls, nrls = norm_Rational}, |
388 crls=Atools_erls, nrls = norm_Rational}, |
381 "Script DiffScr (f_::real) (v_v::real) = " ^ |
389 "Script DiffScr (f_f::real) (v_v::real) = " ^ |
382 " (let f'_ = Take (d_d v_v f_) " ^ |
390 " (let f_f' = Take (d_d v_v f_f) " ^ |
383 " in ((Try (Rewrite_Set norm_Rational False)) @@ " ^ |
391 " in ((Try (Rewrite_Set norm_Rational False)) @@ " ^ |
384 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^ |
392 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^ |
385 " (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^ |
393 " (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^ |
386 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^ |
394 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^ |
387 " (Try (Rewrite_Set norm_Rational False))) f'_)" |
395 " (Try (Rewrite_Set norm_Rational False))) f_f')" |
388 )); |
396 )); |
389 |
397 |
390 |
398 |
391 (** CAS-commands **) |
399 (** CAS-commands **) |
392 |
400 |
396 *) |
404 *) |
397 fun argl2dtss [Const ("Pair", _) $ t $ bdv] = |
405 fun argl2dtss [Const ("Pair", _) $ t $ bdv] = |
398 [((term_of o the o (parse thy)) "functionTerm", [t]), |
406 [((term_of o the o (parse thy)) "functionTerm", [t]), |
399 ((term_of o the o (parse thy)) "differentiateFor", [bdv]), |
407 ((term_of o the o (parse thy)) "differentiateFor", [bdv]), |
400 ((term_of o the o (parse thy)) "derivative", |
408 ((term_of o the o (parse thy)) "derivative", |
401 [(term_of o the o (parse thy)) "f_'_"]) |
409 [(term_of o the o (parse thy)) "f_f'"]) |
402 ] |
410 ] |
403 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss"; |
411 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss"; |
404 castab := |
412 castab := |
405 overwritel (!castab, |
413 overwritel (!castab, |
406 [((term_of o the o (parse thy)) "Diff", |
414 [((term_of o the o (parse thy)) "Diff", |
414 *) |
422 *) |
415 fun argl2dtss [Const ("Pair", _) $ t $ bdv] = |
423 fun argl2dtss [Const ("Pair", _) $ t $ bdv] = |
416 [((term_of o the o (parse thy)) "functionEq", [t]), |
424 [((term_of o the o (parse thy)) "functionEq", [t]), |
417 ((term_of o the o (parse thy)) "differentiateFor", [bdv]), |
425 ((term_of o the o (parse thy)) "differentiateFor", [bdv]), |
418 ((term_of o the o (parse thy)) "derivativeEq", |
426 ((term_of o the o (parse thy)) "derivativeEq", |
419 [(term_of o the o (parse thy)) "f_'_::bool"]) |
427 [(term_of o the o (parse thy)) "f_f'::bool"]) |
420 ] |
428 ] |
421 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss"; |
429 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss"; |
422 castab := |
430 castab := |
423 overwritel (!castab, |
431 overwritel (!castab, |
424 [((term_of o the o (parse thy)) "Differentiate", |
432 [((term_of o the o (parse thy)) "Differentiate", |