# HG changeset patch
# User wenzelm
# Date 1378462920 -7200
# Node ID 92da725a248f0405ab884b09cee6d11151a3f158
# Parent  3b356b7f7cade8ca193f81343252b9e058e8d906
removed junk;

diff -r 3b356b7f7cad -r 92da725a248f src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 06 12:05:01 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 06 12:22:00 2013 +0200
@@ -2656,7 +2656,6 @@
       using goal1(2) B
       apply auto
       done
-      thm has_integralD[OF goal1(1) *]
     obtain g where g:
       "gauge g"
       "\<And>p. p tagged_division_of {a..b} \<Longrightarrow> g fine p \<Longrightarrow>