src/HOL/IMP/Abs_Int3.thy

--- a/src/HOL/IMP/Abs_Int3.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,12 +1,11 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Widening and Narrowing"
+
 theory Abs_Int3
 imports Abs_Int2_ivl
 begin
 
-
-subsection "Widening and Narrowing"
-
 class widen =
 fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)