--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sat Apr 24 11:11:09 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sat Apr 24 13:31:52 2010 -0700
@@ -1350,7 +1350,7 @@
using assms by auto
text {*Still more general form; could derive this directly without using the
- rather involved HOMEOMORPHIC_CONVEX_COMPACT theorem, just using
+ rather involved @{text "HOMEOMORPHIC_CONVEX_COMPACT"} theorem, just using
a scaling and translation to put the set inside the unit cube. *}
lemma brouwer: fixes f::"real^'n \<Rightarrow> real^'n"