src/HOL/Hyperreal/MacLaurin.thy
 changeset 19765 dfe940911617 parent 16924 04246269386e child 20217 25b068a99d2b
```     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Fri Jun 02 20:12:59 2006 +0200
1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Fri Jun 02 23:22:29 2006 +0200
1.3 @@ -31,18 +31,24 @@
1.4  text{*A crude tactic to differentiate by proof.*}
1.5  ML
1.6  {*
1.7 +local
1.8 +val deriv_rulesI =
1.9 +  [thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
1.10 +  thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow",
1.11 +  thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus",
1.12 +  thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow",
1.13 +  thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos",
1.14 +  thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos"];
1.15 +
1.16 +val DERIV_chain2 = thm "DERIV_chain2";
1.17 +
1.18 +in
1.19 +
1.20  exception DERIV_name;
1.21  fun get_fun_name (_ \$ (Const ("Lim.deriv",_) \$ Abs(_,_, Const (f,_) \$ _) \$ _ \$ _)) = f
1.22  |   get_fun_name (_ \$ (_ \$ (Const ("Lim.deriv",_) \$ Abs(_,_, Const (f,_) \$ _) \$ _ \$ _))) = f
1.23  |   get_fun_name _ = raise DERIV_name;
1.24
1.25 -val deriv_rulesI = [DERIV_Id,DERIV_const,DERIV_cos,DERIV_cmult,
1.26 -                    DERIV_sin, DERIV_exp, DERIV_inverse,DERIV_pow,
1.27 -                    DERIV_add, DERIV_diff, DERIV_mult, DERIV_minus,
1.28 -                    DERIV_inverse_fun,DERIV_quotient,DERIV_fun_pow,
1.29 -                    DERIV_fun_exp,DERIV_fun_sin,DERIV_fun_cos,
1.30 -                    DERIV_Id,DERIV_const,DERIV_cos];
1.31 -
1.32  val deriv_tac =
1.33    SUBGOAL (fn (prem,i) =>
1.34     (resolve_tac deriv_rulesI i) ORELSE
1.35 @@ -50,6 +56,8 @@
1.36                       DERIV_chain2) i) handle DERIV_name => no_tac));;
1.37
1.38  val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i));
1.39 +
1.40 +end
1.41  *}
1.42
1.43  lemma Maclaurin_lemma2:
```