--- a/src/HOL/Topological_Spaces.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy Fri Feb 21 00:09:56 2014 +0100
@@ -1298,7 +1298,7 @@
assume *: "\<forall>n. \<exists>p. ?P p n"
def f \<equiv> "rec_nat (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
- have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.recs(2) ..
+ have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.rec(2) ..
have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
then have "subseq f" unfolding subseq_Suc_iff by auto
@@ -1320,7 +1320,7 @@
then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
def f \<equiv> "rec_nat (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
- have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.recs(2) ..
+ have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.rec(2) ..
have P_0: "?P (f 0) (Suc N)"
unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
{ fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"