src/HOL/Hilbert_Choice.thy
changeset 55415 05f5fdb8d093
parent 55088 57c82e01022b
child 55811 aa1acc25126b
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -289,7 +289,7 @@
     1.4    shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
     1.5    -- {* Courtesy of Stephan Merz *}
     1.6  proof -
     1.7 -  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
     1.8 +  def Sseq \<equiv> "rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
     1.9    def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
    1.10    { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
    1.11    moreover then have *: "\<And>n. pick n \<in> Sseq n" by (metis someI_ex pick_def ex_in_conv finite.simps)
    1.12 @@ -534,8 +534,8 @@
    1.13   apply (erule exE)
    1.14   apply (erule_tac x = "{w. \<exists>i. w=f i}" in allE, blast)
    1.15  apply (erule contrapos_np, simp, clarify)
    1.16 -apply (subgoal_tac "\<forall>n. nat_rec x (%i y. @z. z:Q & (z,y) :r) n \<in> Q")
    1.17 - apply (rule_tac x = "nat_rec x (%i y. @z. z:Q & (z,y) :r)" in exI)
    1.18 +apply (subgoal_tac "\<forall>n. rec_nat x (%i y. @z. z:Q & (z,y) :r) n \<in> Q")
    1.19 + apply (rule_tac x = "rec_nat x (%i y. @z. z:Q & (z,y) :r)" in exI)
    1.20   apply (rule allI, simp)
    1.21   apply (rule someI2_ex, blast, blast)
    1.22  apply (rule allI)