diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Collecting.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,8 +1,12 @@
+(* Author: Tobias Nipkow *)
+
+subsection "Collecting Semantics of Commands"
+
 theory Collecting
 imports Complete_Lattice Big_Step ACom
 begin
 
-subsection "The generic Step function"
+subsubsection "The generic Step function"
 
 notation
   sup (infixl "\<squnion>" 65) and
@@ -30,8 +34,6 @@
 by(induct C arbitrary: S) auto
 
 
-subsection "Collecting Semantics of Commands"
-
 subsubsection "Annotated commands as a complete lattice"
 
 instantiation acom :: (order) order