diff -r 262572d90bc6 -r f962e42e324d src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -4,7 +4,7 @@
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 *)
 
-header{*Construction of Hyperreals Using Ultrafilters*}
+section{*Construction of Hyperreals Using Ultrafilters*}
 
 theory HyperDef
 imports Complex_Main HyperNat