# HG changeset patch
# User haftmann
# Date 1282899320 -7200
# Node ID 2d638e963357cd6fcb84cca722a5dedf78582465
# Parent  ec9a4926e3c6aa7aab45666cc84b8ce2591cf5bf
tuned fact reference

diff -r ec9a4926e3c6 -r 2d638e963357 src/HOL/Multivariate_Analysis/Gauge_Measure.thy
--- a/src/HOL/Multivariate_Analysis/Gauge_Measure.thy	Thu Aug 26 21:03:14 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Gauge_Measure.thy	Fri Aug 27 10:55:20 2010 +0200
@@ -311,7 +311,7 @@
   shows "(\<Union> f) has_gmeasure (setsum m f)" using assms
 proof induct case (insert x s)
   have *:"(x \<inter> \<Union>s) = \<Union>{x \<inter> y| y. y\<in>s}"by auto
-  show ?case unfolding Union_insert ring_class.setsum.insert[OF insert(1-2)] 
+  show ?case unfolding Union_insert setsum.insert [OF insert(1-2)] 
     apply(rule has_gmeasure_negligible_union) unfolding *
     apply(rule insert) defer apply(rule insert) apply(rule insert) defer
     apply(rule insert) prefer 4 apply(rule negligible_unions)