--- 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) |
--- 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"
--- 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