# HG changeset patch
# User nipkow
# Date 1326644866 -3600
# Node ID d0a2c4a80a00f499c5ab4eee921cac7636017423
# Parent  426ed18eba433c6a1409481cfcfc3d12c02e6c08
tuned

diff -r 426ed18eba43 -r d0a2c4a80a00 src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Sat Jan 14 21:16:15 2012 +0100
+++ b/src/HOL/IMP/ACom.thy	Sun Jan 15 17:27:46 2012 +0100
@@ -7,7 +7,7 @@
 (* is there a better place? *)
 definition "show_state xs s = [(x,s x). x \<leftarrow> xs]"
 
-section "Annotated Commands"
+subsection "Annotated Commands"
 
 datatype 'a acom =
   SKIP   'a                           ("SKIP {_}" 61) |
diff -r 426ed18eba43 -r d0a2c4a80a00 src/HOL/IMP/Abs_Int0_fun.thy
--- a/src/HOL/IMP/Abs_Int0_fun.thy	Sat Jan 14 21:16:15 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy	Sun Jan 15 17:27:46 2012 +0100
@@ -1,7 +1,5 @@
 (* Author: Tobias Nipkow *)
 
-header "Abstract Interpretation"
-
 theory Abs_Int0_fun
 imports "~~/src/HOL/ex/Interpretation_with_Defs"
         "~~/src/HOL/Library/While_Combinator"
diff -r 426ed18eba43 -r d0a2c4a80a00 src/HOL/IMP/Complete_Lattice_ix.thy
--- a/src/HOL/IMP/Complete_Lattice_ix.thy	Sat Jan 14 21:16:15 2012 +0100
+++ b/src/HOL/IMP/Complete_Lattice_ix.thy	Sun Jan 15 17:27:46 2012 +0100
@@ -1,7 +1,13 @@
+(* Author: Tobias Nipkow *)
+
+header "Abstract Interpretation"
+
 theory Complete_Lattice_ix
 imports Main
 begin
 
+subsection "Complete Lattice (indexed)"
+
 text{* A complete lattice is an ordered type where every set of elements has
 a greatest lower (and thus also a leats upper) bound. Sets are the
 prototypical complete lattice where the greatest lower bound is