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/Finite_Product_Measure.thy
changeset 50245 dea9363887a6
parent 50244 de72bbe42190
child 50387 3d8863c41fe8 
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 27 13:48:40 2012 +0100
@@ -178,7 +178,7 @@
 
 lemma prod_algebra_sets_into_space:
   "prod_algebra I M \<subseteq> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
-  using assms by (auto simp: prod_emb_def prod_algebra_def)
+  by (auto simp: prod_emb_def prod_algebra_def)
 
 lemma prod_algebra_eq_finite:
   assumes I: "finite I"
isabelle