diff -r eec472dae593 -r 154dc6ec0041 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Mon Mar 12 21:41:11 2012 +0100
@@ -1417,7 +1417,7 @@
proof
fix a
have "?sup -` {a<..} \ space M = (\i\A. {x\space M. a < f i x})"
- by (auto simp: less_SUP_iff SUP_apply)
+ by (auto simp: less_SUP_iff)
then show "?sup -` {a<..} \ space M \ sets M"
using assms by auto
qed
@@ -1430,7 +1430,7 @@
proof
fix a
have "?inf -` {.. space M = (\i\A. {x\space M. f i x < a})"
- by (auto simp: INF_less_iff INF_apply)
+ by (auto simp: INF_less_iff)
then show "?inf -` {.. space M \ sets M"
using assms by auto
qed