changeset 58877 | 262572d90bc6 |
parent 57418 | 6ab1c7cb0b8d |
child 59765 | 26d1c71784f1 |
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sun Nov 02 17:06:05 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sun Nov 02 17:09:04 2014 +0100 @@ -16,7 +16,7 @@ (* (c) Copyright, John Harrison 1998-2008 *) (* ========================================================================= *) -header {* Results connected with topological dimension. *} +section {* Results connected with topological dimension. *} theory Brouwer_Fixpoint imports Convex_Euclidean_Space