--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Mon Dec 06 19:18:02 2010 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Fri Dec 03 15:25:14 2010 +0100
@@ -274,7 +274,7 @@
"snd ` (SIGMA x:f`X. f -` {x} \<inter> X) = X"
by (auto simp: image_iff)
-lemma zero_le_eq_True: "0 \<le> (x::pinfreal) \<longleftrightarrow> True" by simp
+lemma zero_le_eq_True: "0 \<le> (x::pextreal) \<longleftrightarrow> True" by simp
lemma Real_setprod:
assumes"\<And>i. i\<in>X \<Longrightarrow> 0 \<le> f i"