--- a/src/HOL/Probability/Radon_Nikodym.thy Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Fri Feb 21 00:09:56 2014 +0100
@@ -250,7 +250,7 @@
{ fix i have "A i \<in> sets M" unfolding A_def
proof (induct i)
case (Suc i)
- from Ex_P[OF this, of i] show ?case unfolding nat.recs(2)
+ from Ex_P[OF this, of i] show ?case unfolding nat.rec(2)
by (rule someI2_ex) simp
qed simp }
note A_in_sets = this
@@ -281,7 +281,7 @@
from ex_inverse_of_nat_Suc_less[OF this]
obtain n where *: "?d B < - 1 / real (Suc n)"
by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
- have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.recs(2))
+ have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.rec(2))
from epsilon[OF B(1) this] *
show False by auto
qed