equal
deleted
inserted
replaced
98 |
98 |
99 (** eval functions **) |
99 (** eval functions **) |
100 |
100 |
101 fun primed (Const (id, T)) = Const (id ^ "'", T) |
101 fun primed (Const (id, T)) = Const (id ^ "'", T) |
102 | primed (Free (id, T)) = Free (id ^ "'", T) |
102 | primed (Free (id, T)) = Free (id ^ "'", T) |
103 | primed t = raise error ("primed called with arg = '"^ term2str t ^"'"); |
103 | primed t = error ("primed called with arg = '"^ term2str t ^"'"); |
104 |
104 |
105 (*("primed", ("Diff.primed", eval_primed "#primed"))*) |
105 (*("primed", ("Diff.primed", eval_primed "#primed"))*) |
106 fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ = |
106 fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ = |
107 SOME ((term2str p) ^ " = " ^ term2str (primed t), |
107 SOME ((term2str p) ^ " = " ^ term2str (primed t), |
108 Trueprop $ (mk_equality (p, primed t))) |
108 Trueprop $ (mk_equality (p, primed t))) |
406 [((term_of o the o (parse thy)) "functionTerm", [t]), |
406 [((term_of o the o (parse thy)) "functionTerm", [t]), |
407 ((term_of o the o (parse thy)) "differentiateFor", [bdv]), |
407 ((term_of o the o (parse thy)) "differentiateFor", [bdv]), |
408 ((term_of o the o (parse thy)) "derivative", |
408 ((term_of o the o (parse thy)) "derivative", |
409 [(term_of o the o (parse thy)) "f_f'"]) |
409 [(term_of o the o (parse thy)) "f_f'"]) |
410 ] |
410 ] |
411 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss"; |
411 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss"; |
412 castab := |
412 castab := |
413 overwritel (!castab, |
413 overwritel (!castab, |
414 [((term_of o the o (parse thy)) "Diff", |
414 [((term_of o the o (parse thy)) "Diff", |
415 (("Isac", ["derivative_of","function"], ["no_met"]), |
415 (("Isac", ["derivative_of","function"], ["no_met"]), |
416 argl2dtss)) |
416 argl2dtss)) |
424 [((term_of o the o (parse thy)) "functionEq", [t]), |
424 [((term_of o the o (parse thy)) "functionEq", [t]), |
425 ((term_of o the o (parse thy)) "differentiateFor", [bdv]), |
425 ((term_of o the o (parse thy)) "differentiateFor", [bdv]), |
426 ((term_of o the o (parse thy)) "derivativeEq", |
426 ((term_of o the o (parse thy)) "derivativeEq", |
427 [(term_of o the o (parse thy)) "f_f'::bool"]) |
427 [(term_of o the o (parse thy)) "f_f'::bool"]) |
428 ] |
428 ] |
429 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss"; |
429 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss"; |
430 castab := |
430 castab := |
431 overwritel (!castab, |
431 overwritel (!castab, |
432 [((term_of o the o (parse thy)) "Differentiate", |
432 [((term_of o the o (parse thy)) "Differentiate", |
433 (("Isac", ["named","derivative_of","function"], ["no_met"]), |
433 (("Isac", ["named","derivative_of","function"], ["no_met"]), |
434 argl2dtss)) |
434 argl2dtss)) |