Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Probability/Sigma_Algebra.thy
changeset 40702 cf26dd7395e4
parent 39960 03174b2d075c
child 40859 de0b30e6c2d2 
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -132,7 +132,7 @@
       by (auto intro!: exI[of _ "from_nat i"])
   qed
   have **: "range ?A' = range A"
-    using surj_range[OF surj_from_nat]
+    using surj_from_nat
     by (auto simp: image_compose intro!: imageI)
   show ?thesis unfolding * ** ..
 qed
isabelle