# HG changeset patch
# User wenzelm
# Date 1236208588 -3600
# Node ID 5af6ed62385b60dc4eabe73aa405457975d5a33b
# Parent  171b3bd93c905aa65bf63e558e1ef0e2954bde0c
fixed document;

diff -r 171b3bd93c90 -r 5af6ed62385b src/HOL/Library/Topology_Euclidean_Space.thy
--- 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"