src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
changeset 41023 9118eb4eb8dc
parent 40859 de0b30e6c2d2
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Mon Dec 06 19:18:02 2010 +0100
     1.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Fri Dec 03 15:25:14 2010 +0100
     1.3 @@ -274,7 +274,7 @@
     1.4    "snd ` (SIGMA x:f`X. f -` {x} \<inter> X) = X"
     1.5    by (auto simp: image_iff)
     1.6  
     1.7 -lemma zero_le_eq_True: "0 \<le> (x::pinfreal) \<longleftrightarrow> True" by simp
     1.8 +lemma zero_le_eq_True: "0 \<le> (x::pextreal) \<longleftrightarrow> True" by simp
     1.9  
    1.10  lemma Real_setprod:
    1.11    assumes"\<And>i. i\<in>X \<Longrightarrow> 0 \<le> f i"