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/Borel.thy
changeset 37591 d3daea901123
parent 37032 58a0757031dd
child 37887 2ae085b07f2f 
--- a/src/HOL/Probability/Borel.thy	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Probability/Borel.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -203,7 +203,7 @@
         by (metis surj_def)
 
       from Fract i j n show ?thesis
-        by (metis prod.cases prod_case_split)
+        by (metis prod.cases)
   qed
 qed
isabelle