changeset 69517 | dc20f278e8f3 |
parent 69173 | 38beaaebe736 |
child 69677 | a06b204527e6 |
--- a/src/HOL/Analysis/Fashoda_Theorem.thy Thu Dec 27 23:38:55 2018 +0100 +++ b/src/HOL/Analysis/Fashoda_Theorem.thy Fri Dec 28 10:29:59 2018 +0100 @@ -2,7 +2,7 @@ Author: Robert Himmelmann, TU Muenchen (translation from HOL light) *) -section%important \<open>Fashoda meet theorem\<close> +section%important \<open>Fashoda Meet Theorem\<close> theory Fashoda_Theorem imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space