# HG changeset patch
# User huffman
# Date 1162397656 -3600
# Node ID 1c0805003c4fe6f749478640fa0996f27fca9d07
# Parent  c957e02e7a36f019d1f4ea92dc8160237a32aa99
generalize type of lemma isCont_Id

diff -r c957e02e7a36 -r 1c0805003c4f src/HOL/Hyperreal/Lim.thy
--- 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)