src/HOL/Hyperreal/MacLaurin.thy
changeset 23069 cdfff0241c12
parent 22985 501e6dfe4e5a
child 23177 3004310c95b1
--- a/src/HOL/Hyperreal/MacLaurin.thy	Tue May 22 05:07:48 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue May 22 07:29:49 2007 +0200
@@ -33,12 +33,12 @@
 {*
 local
 val deriv_rulesI =
-  [thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
+  [thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
   thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow",
   thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus",
   thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow",
   thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos",
-  thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos"];
+  thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos"];
 
 val DERIV_chain2 = thm "DERIV_chain2";
 
@@ -251,7 +251,7 @@
 apply (rule DERIV_cmult)
 apply (rule lemma_DERIV_subst)
 apply (rule DERIV_chain2 [where g=uminus])
-apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_Id)
+apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_ident)
 prefer 2 apply force
 apply force
 apply (rule_tac x = "-t" in exI, auto)