--- a/src/HOL/IMP/Abs_Int1_const.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,11 +1,11 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Constant Propagation"
+
 theory Abs_Int1_const
 imports Abs_Int1
 begin
 
-subsection "Constant Propagation"
-
 datatype const = Const val | Any
 
 fun \<gamma>_const where