# HG changeset patch
# User nipkow
# Date 1534865386 -7200
# Node ID 4566bac4517dff708d12ff4169baabdefd7bdc58
# Parent  d505274da8015d3757e0956068a14ff2cff11fd5
improved sectioning

diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/ACom.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,11 +1,11 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Annotated Commands"
+
 theory ACom
 imports Com
 begin
 
-subsection "Annotated Commands"
-
 datatype 'a acom =
   SKIP 'a                           ("SKIP {_}" 61) |
   Assign vname aexp 'a              ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,10 +1,12 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Abstract Interpretation"
+
 theory Abs_Int0
 imports Abs_Int_init
 begin
 
-subsection "Orderings"
+subsubsection "Orderings"
 
 text\<open>The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are
 defined in @{theory Main}, more precisely in theories @{theory HOL.Orderings} and @{theory HOL.Lattices}.
@@ -139,7 +141,7 @@
 using pfp_inv[OF assms(2), where P = "%x. g x = g x0"] assms(1) by simp
 
 
-subsection "Abstract Interpretation"
+subsubsection "Abstract Interpretation"
 
 definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
 "\<gamma>_fun \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(F x)}"
diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,11 +1,11 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Computable Abstract Interpretation"
+
 theory Abs_Int1
 imports Abs_State
 begin
 
-subsection "Computable Abstract Interpretation"
-
 text\<open>Abstract interpretation over type @{text st} instead of functions.\<close>
 
 context Gamma_semilattice
diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,11 +1,11 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Constant Propagation"
+
 theory Abs_Int1_const
 imports Abs_Int1
 begin
 
-subsection "Constant Propagation"
-
 datatype const = Const val | Any
 
 fun \<gamma>_const where
diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,11 +1,11 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Parity Analysis"
+
 theory Abs_Int1_parity
 imports Abs_Int1
 begin
 
-subsection "Parity Analysis"
-
 datatype parity = Even | Odd | Either
 
 text\<open>Instantiation of class @{class order} with type @{typ parity}:\<close>
diff -r d505274da801 -r 4566bac4517d 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 ..
 
diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,11 +1,11 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Interval Analysis"
+
 theory Abs_Int2_ivl
 imports Abs_Int2
 begin
 
-subsection "Interval Analysis"
-
 type_synonym eint = "int extended"
 type_synonym eint2 = "eint * eint"
 
diff -r d505274da801 -r 4566bac4517d 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)
 
diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Abs_Int_Tests.thy
--- a/src/HOL/IMP/Abs_Int_Tests.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int_Tests.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,9 +1,11 @@
+(* Author: Tobias Nipkow *)
+
+subsection "Abstract Interpretation Test Programs"
+
 theory Abs_Int_Tests
 imports Com
 begin
 
-subsection "Test Programs"
-
 text\<open>For constant propagation:\<close>
 
 text\<open>Straight line code:\<close>
diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,5 +1,7 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Computable State"
+
 theory Abs_State
 imports Abs_Int0
 begin
diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Collecting.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,8 +1,12 @@
+(* Author: Tobias Nipkow *)
+
+subsection "Collecting Semantics of Commands"
+
 theory Collecting
 imports Complete_Lattice Big_Step ACom
 begin
 
-subsection "The generic Step function"
+subsubsection "The generic Step function"
 
 notation
   sup (infixl "\<squnion>" 65) and
@@ -30,8 +34,6 @@
 by(induct C arbitrary: S) auto
 
 
-subsection "Collecting Semantics of Commands"
-
 subsubsection "Annotated commands as a complete lattice"
 
 instantiation acom :: (order) order
diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Collecting1.thy
--- a/src/HOL/IMP/Collecting1.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Collecting1.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,9 +1,9 @@
+subsection "A small step semantics on annotated commands"
+
 theory Collecting1
 imports Collecting
 begin
 
-subsection "A small step semantics on annotated commands"
-
 text\<open>The idea: the state is propagated through the annotated command as an
 annotation @{term "{s}"}, all other annotations are @{term "{}"}. It is easy
 to show that this semantics approximates the collecting semantics.\<close>
diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Collecting_Examples.thy
--- a/src/HOL/IMP/Collecting_Examples.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Collecting_Examples.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,8 +1,10 @@
+subsection "Collecting Semantics Examples"
+
 theory Collecting_Examples
 imports Collecting Vars
 begin
 
-subsection "Pretty printing state sets"
+subsubsection "Pretty printing state sets"
 
 text\<open>Tweak code generation to work with sets of non-equality types:\<close>
 declare insert_code[code del] union_coset_filter[code del]
@@ -27,7 +29,7 @@
    annotate (\<lambda>p. (\<lambda>s. (\<lambda>x. (x, s x)) ` (vars_acom C)) ` anno C p) (strip C)"
 
 
-subsection "Examples"
+subsubsection "Examples"
 
 definition "c0 = WHILE Less (V ''x'') (N 3)
                 DO ''x'' ::= Plus (V ''x'') (N 2)"
diff -r d505274da801 -r 4566bac4517d src/HOL/IMP/Complete_Lattice.thy
--- a/src/HOL/IMP/Complete_Lattice.thy	Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Complete_Lattice.thy	Tue Aug 21 17:29:46 2018 +0200
@@ -1,5 +1,9 @@
+(* Author: Tobias Nipkow *)
+
 section "Abstract Interpretation"
 
+subsection "Complete Lattice"
+
 theory Complete_Lattice
 imports Main
 begin