src/HOL/Probability/Radon_Nikodym.thy
changeset 55642 63beb38e9258
parent 55417 01fbfb60c33e
child 56166 9a241bc276cd
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Feb 21 00:09:55 2014 +0100
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Feb 21 00:09:56 2014 +0100
     1.3 @@ -250,7 +250,7 @@
     1.4    { fix i have "A i \<in> sets M" unfolding A_def
     1.5      proof (induct i)
     1.6        case (Suc i)
     1.7 -      from Ex_P[OF this, of i] show ?case unfolding nat.recs(2)
     1.8 +      from Ex_P[OF this, of i] show ?case unfolding nat.rec(2)
     1.9          by (rule someI2_ex) simp
    1.10      qed simp }
    1.11    note A_in_sets = this
    1.12 @@ -281,7 +281,7 @@
    1.13        from ex_inverse_of_nat_Suc_less[OF this]
    1.14        obtain n where *: "?d B < - 1 / real (Suc n)"
    1.15          by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
    1.16 -      have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.recs(2))
    1.17 +      have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.rec(2))
    1.18        from epsilon[OF B(1) this] *
    1.19        show False by auto
    1.20      qed