src/HOL/Topological_Spaces.thy
 changeset 55415 05f5fdb8d093 parent 54797 be020ec8560c child 55417 01fbfb60c33e
```     1.1 --- a/src/HOL/Topological_Spaces.thy	Wed Feb 12 08:35:57 2014 +0100
1.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Feb 12 08:35:57 2014 +0100
1.3 @@ -1296,7 +1296,7 @@
1.4  proof cases
1.5    let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)"
1.6    assume *: "\<forall>n. \<exists>p. ?P p n"
1.7 -  def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
1.8 +  def f \<equiv> "rec_nat (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
1.9    have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
1.10    have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
1.11    have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
1.12 @@ -1318,7 +1318,7 @@
1.13    let "?P p m" = "m < p \<and> s m < s p"
1.14    assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
1.15    then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
1.16 -  def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
1.17 +  def f \<equiv> "rec_nat (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
1.18    have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
1.19    have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
1.20    have P_0: "?P (f 0) (Suc N)"
```