Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Hyperreal/MacLaurin.thy
changeset 23069 cdfff0241c12
parent 22985 501e6dfe4e5a
child 23177 3004310c95b1 
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Tue May 22 05:07:48 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue May 22 07:29:49 2007 +0200
     1.3 @@ -33,12 +33,12 @@
     1.4  {*
     1.5  local
     1.6  val deriv_rulesI =
     1.7 -  [thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
     1.8 +  [thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
     1.9    thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow",
    1.10    thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus",
    1.11    thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow",
    1.12    thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos",
    1.13 -  thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos"];
    1.14 +  thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos"];
    1.15  
    1.16  val DERIV_chain2 = thm "DERIV_chain2";
    1.17  
    1.18 @@ -251,7 +251,7 @@
    1.19  apply (rule DERIV_cmult)
    1.20  apply (rule lemma_DERIV_subst)
    1.21  apply (rule DERIV_chain2 [where g=uminus])
    1.22 -apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_Id)
    1.23 +apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_ident)
    1.24  prefer 2 apply force
    1.25  apply force
    1.26  apply (rule_tac x = "-t" in exI, auto)
isabelle