diff -r eba74a5790d2 -r 3578434d645d src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Tue Jun 30 18:21:55 2009 +0200
+++ b/src/HOL/MacLaurin.thy	Tue Jun 30 18:24:00 2009 +0200
@@ -27,36 +27,6 @@
 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
 by arith
 
-text{*A crude tactic to differentiate by proof.*}
-
-lemmas deriv_rulesI =
-  DERIV_ident DERIV_const DERIV_cos DERIV_cmult
-  DERIV_sin DERIV_exp DERIV_inverse DERIV_pow
-  DERIV_add DERIV_diff DERIV_mult DERIV_minus
-  DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
-  DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
-  DERIV_ident DERIV_const DERIV_cos
-
-ML
-{*
-local
-exception DERIV_name;
-fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
-|   get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
-|   get_fun_name _ = raise DERIV_name;
-
-in
-
-fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
-  resolve_tac @{thms deriv_rulesI} i ORELSE
-    ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)]
-                     @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
-
-fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
-
-end
-*}
-
 lemma Maclaurin_lemma2:
   assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   assumes n: "n = Suc k"
@@ -97,7 +67,6 @@
  apply (simp add: mult_ac)
 done
 
-
 lemma Maclaurin:
   assumes h: "0 < h"
   assumes n: "0 < n"