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)"