| changeset 37674 | f86de9c00c47 |
| parent 37489 | 44e42d392c6e |
| child 39302 | d7728f65b353 |
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Jul 01 09:24:04 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Jul 01 15:40:38 2010 -0700 @@ -4,7 +4,7 @@ header {* Fashoda meet theorem. *} theory Fashoda -imports Brouwer_Fixpoint Path_Connected +imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space begin subsection {*Fashoda meet theorem. *}