--- a/src/HOL/Library/Topology_Euclidean_Space.thy Wed Mar 04 23:52:47 2009 +0100
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Thu Mar 05 00:16:28 2009 +0100
@@ -2421,7 +2421,7 @@
using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] by auto
qed
-subsection{* Heine-Borel theorem (following Burkill & Burkill vol. 2) *}
+subsection{* Heine-Borel theorem (following Burkill \& Burkill vol. 2) *}
lemma heine_borel_lemma: fixes s::"(real^'n) set"
assumes "compact s" "s \<subseteq> (\<Union> t)" "\<forall>b \<in> t. open b"