src/HOL/NSA/StarDef.thy

--- a/src/HOL/NSA/StarDef.thy	Sun Nov 02 17:09:04 2014 +0100
+++ b/src/HOL/NSA/StarDef.thy	Sun Nov 02 17:13:28 2014 +0100
@@ -2,7 +2,7 @@
     Author      : Jacques D. Fleuriot and Brian Huffman
 *)
 
-header {* Construction of Star Types Using Ultrafilters *}
+section {* Construction of Star Types Using Ultrafilters *}
 
 theory StarDef
 imports Filter