src/HOL/Lim.thy
changeset 41550 efa734d9b221
parent 37767 a2b7a20d6ea3
child 44194 0639898074ae
     1.1 --- a/src/HOL/Lim.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/Lim.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -653,7 +653,7 @@
     1.4    moreover have "\<forall>n. ?F n \<noteq> a"
     1.5      by (rule allI) (rule F1)
     1.6  
     1.7 -  moreover from prems have "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by simp
     1.8 +  moreover note `\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L`
     1.9    ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp
    1.10    
    1.11    moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"