src/HOL/Probability/Infinite_Product_Measure.thy
changeset 55642 63beb38e9258
parent 55417 01fbfb60c33e
child 56996 891e992e510f
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Feb 21 00:09:55 2014 +0100
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Feb 21 00:09:56 2014 +0100
     1.3 @@ -196,7 +196,7 @@
     1.4            (\<forall>n. ?a / 2 ^ (k + 1) \<le> ?q k n (w k)) \<and> (k \<noteq> 0 \<longrightarrow> restrict (w k) (J (k - 1)) = w (k - 1))"
     1.5          proof (induct k)
     1.6            case 0 with w0 show ?case
     1.7 -            unfolding w_def nat.recs(1) by auto
     1.8 +            unfolding w_def nat.rec(1) by auto
     1.9          next
    1.10            case (Suc k)
    1.11            then have wk: "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
    1.12 @@ -241,7 +241,7 @@
    1.13                   (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
    1.14            qed
    1.15            then have "?P k (w k) (w (Suc k))"
    1.16 -            unfolding w_def nat.recs(2) unfolding w_def[symmetric]
    1.17 +            unfolding w_def nat.rec(2) unfolding w_def[symmetric]
    1.18              by (rule someI_ex)
    1.19            then show ?case by auto
    1.20          qed