diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Table.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Table.thy
     Author:     David von Oheimb
 *)
-header {* Abstract tables and their implementation as lists *}
+subsection {* Abstract tables and their implementation as lists *}
 
 theory Table imports Basis begin
 
@@ -35,7 +35,7 @@
       = "'a \<Rightarrow> 'b set"
 
 
-section "map of / table of"
+subsubsection "map of / table of"
 
 abbreviation
   table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"   --{* concrete table *}
@@ -49,7 +49,7 @@
   by (simp add: map_add_def)
 
 
-section {* Conditional Override *}
+subsubsection {* Conditional Override *}
 
 definition cond_override :: "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" where
 
@@ -95,7 +95,7 @@
 by (rule finite_UnI)
 
 
-section {* Filter on Tables *}
+subsubsection {* Filter on Tables *}
 
 definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"
   where
@@ -179,7 +179,7 @@
 by (auto simp add: fun_eq_iff cond_override_def filter_tab_def )
 
 
-section {* Misc *}
+subsubsection {* Misc *}
 
 lemma Ball_set_table: "(\<forall> (x,y)\<in> set l. P x y) \<Longrightarrow> \<forall> x. \<forall> y\<in> map_of l x: P x y"
 apply (erule rev_mp)
@@ -289,7 +289,7 @@
   where "(t hiding  s under C entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y)"
 
 
-section "Untables"
+subsubsection "Untables"
 
 lemma Un_tablesI [intro]:  "t \<in> ts \<Longrightarrow> x \<in> t k \<Longrightarrow> x \<in> Un_tables ts k"
   by (auto simp add: Un_tables_def)
@@ -301,7 +301,7 @@
   by (simp add: Un_tables_def)
 
 
-section "overrides"
+subsubsection "overrides"
 
 lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m"
   by (simp add: overrides_t_def)
@@ -322,7 +322,7 @@
   by (simp add: overrides_t_def)
 
 
-section "hiding entails"
+subsubsection "hiding entails"
 
 lemma hiding_entailsD: 
   "t hiding s entails R \<Longrightarrow> t k = Some x \<Longrightarrow> s k = Some y \<Longrightarrow> R x y"
@@ -335,7 +335,7 @@
   by (simp add: hiding_entails_def)
 
 
-section "cond hiding entails"
+subsubsection "cond hiding entails"
 
 lemma cond_hiding_entailsD: 
 "\<lbrakk>t hiding s under C entails R; t k = Some x; s k = Some y; C x y\<rbrakk> \<Longrightarrow> R x y"