src/HOL/IMP/Abs_Int2.thy

--- a/src/HOL/IMP/Abs_Int2.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,5 +1,7 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Backward Analysis of Expressions"
+
 theory Abs_Int2
 imports Abs_Int1
 begin
@@ -24,7 +26,7 @@
 end
 
 
-subsection "Backward Analysis of Expressions"
+subsubsection "Extended Framework"
 
 subclass (in bounded_lattice) semilattice_sup_top ..