src/HOL/Analysis/Fashoda_Theorem.thy
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