src/HOL/Hyperreal/Lim.thy
changeset 21140 1c0805003c4f
parent 20805 35574b9b59aa
child 21141 f0b5e6254a1f
--- a/src/HOL/Hyperreal/Lim.thy	Wed Nov 01 16:48:58 2006 +0100
+++ b/src/HOL/Hyperreal/Lim.thy	Wed Nov 01 17:14:16 2006 +0100
@@ -551,6 +551,9 @@
 apply (auto intro: isCont_add isCont_minus)
 done
 
+lemma isCont_Id: "isCont (\<lambda>x. x) a"
+by (simp only: isCont_def LIM_self)
+
 lemma isCont_const [simp]: "isCont (%x. k) a"
 by (simp add: isCont_def)
 
@@ -1281,8 +1284,6 @@
 lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db"
 by (auto dest: DERIV_chain simp add: o_def)
 
-lemmas isCont_Id = DERIV_Id [THEN DERIV_isCont, standard]
-
 (*derivative of linear multiplication*)
 lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c"
 by (cut_tac c = c and x = x in DERIV_Id [THEN DERIV_cmult], simp)