# HG changeset patch
# User wenzelm
# Date 1326654239 -3600
# Node ID bed0a3584faf064a1db8813de0179ee7a186a9ac
# Parent  d0a2c4a80a00f499c5ab4eee921cac7636017423# Parent  d8286601e7df9edfe60ad40e1fb23d2533bf6ee4
merged

diff -r d8286601e7df -r bed0a3584faf src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Sun Jan 15 19:55:31 2012 +0100
+++ b/src/HOL/IMP/ACom.thy	Sun Jan 15 20:03:59 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 d8286601e7df -r bed0a3584faf src/HOL/IMP/Abs_Int0_fun.thy
--- a/src/HOL/IMP/Abs_Int0_fun.thy	Sun Jan 15 19:55:31 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy	Sun Jan 15 20:03:59 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 d8286601e7df -r bed0a3584faf src/HOL/IMP/Complete_Lattice_ix.thy
--- a/src/HOL/IMP/Complete_Lattice_ix.thy	Sun Jan 15 19:55:31 2012 +0100
+++ b/src/HOL/IMP/Complete_Lattice_ix.thy	Sun Jan 15 20:03:59 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