| changeset 58889 | 5b7a9633cfa8 |
| parent 58247 | 98d0f85d247f |
| child 61343 | 5b5656a63bd6 |
--- a/src/HOL/ex/Gauge_Integration.thy Sun Nov 02 18:21:14 2014 +0100 +++ b/src/HOL/ex/Gauge_Integration.thy Sun Nov 02 18:21:45 2014 +0100 @@ -4,7 +4,7 @@ Replaced by ~~/src/HOL/Multivariate_Analysis/Real_Integral.thy . *) -header{*Theory of Integration on real intervals*} +section{*Theory of Integration on real intervals*} theory Gauge_Integration imports Complex_Main