--- a/src/HOL/Bali/DefiniteAssignment.thy Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy Sun Nov 02 18:16:19 2014 +0100
@@ -1,4 +1,4 @@
-header {* Definite Assignment *}
+subsection {* Definite Assignment *}
theory DefiniteAssignment imports WellType begin
@@ -39,7 +39,7 @@
\end{itemize}
*}
-section {* Correct nesting of jump statements *}
+subsubsection {* Correct nesting of jump statements *}
text {* For definite assignment it becomes crucial, that jumps (break,
continue, return) are nested correctly i.e. a continue jump is nested in a
@@ -111,7 +111,7 @@
-section {* Calculation of assigned variables for boolean expressions*}
+subsubsection {* Calculation of assigned variables for boolean expressions*}
subsection {* Very restricted calculation fallback calculation *}
@@ -495,7 +495,7 @@
by (unfold all_union_ts_def) blast
-section "The rules of definite assignment"
+subsubsection "The rules of definite assignment"
type_synonym breakass = "(label, lname) tables"