diff -r eacb54d9e78d -r 5818d9cfb2e7 src/HOL/ex/Efficient_Nat_examples.thy
--- a/src/HOL/ex/Efficient_Nat_examples.thy	Tue Oct 07 16:07:33 2008 +0200
+++ b/src/HOL/ex/Efficient_Nat_examples.thy	Tue Oct 07 16:07:40 2008 +0200
@@ -3,7 +3,7 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-header {* Simple examples for Efficient\_Nat theory.  *}
+header {* Simple examples for Efficient\_Nat theory. *}
 
 theory Efficient_Nat_examples
 imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat