
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Probability/Stream_Space.thy
--- a/src/HOL/Probability/Stream_Space.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Probability/Stream_Space.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -238,7 +238,7 @@
   { fix n have "AE x in stream_space M. P (x !! n)"
     proof (induct n)
       case 0 with P show ?case
-        by (subst AE_stream_space) (auto elim!: eventually_elim1)
+        by (subst AE_stream_space) (auto elim!: eventually_mono)
     next
       case (Suc n) then show ?case
         by (subst AE_stream_space) auto




