Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed junk;
authorwenzelm
Fri, 06 Sep 2013 12:22:00 +0200
changeset 53434 92da725a248f
parent 53433 3b356b7f7cad
child 53435 2220f0fb5581
removed junk;
src/HOL/Multivariate_Analysis/Integration.thy file | annotate | diff | comparison | revisions 
--- 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>
isabelle