# HG changeset patch
# User wenzelm
# Date 1414948579 -3600
# Node ID 38db8ddc0f570339ba683abed88dc5c0e502c5d7
# Parent  8a6cac7c724741666647fd17afe4747bc4688098
modernized header;

diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/AxCompl.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb and Norbert Schirmer
 *)
 
-header {*
+subsection {*
 Completeness proof for Axiomatic semantics of Java expressions and statements
 *}
 
@@ -18,7 +18,7 @@
 
 
            
-section "set of not yet initialzed classes"
+subsubsection "set of not yet initialzed classes"
 
 definition
   nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set"
@@ -93,7 +93,7 @@
 done
 
 
-section "init-le"
+subsubsection "init-le"
 
 definition
   init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_"  [51,51] 50)
@@ -113,7 +113,7 @@
 apply (rule card_nyinitcls_bound)
 done
 
-section "Most General Triples and Formulas"
+subsubsection "Most General Triples and Formulas"
 
 definition
   remember_init_state :: "state assn" ("\<doteq>")
@@ -265,7 +265,7 @@
 apply blast
 done
 
-section "main lemmas"
+subsubsection "main lemmas"
 
 lemma MGFn_Init: 
  assumes mgf_hyp: "\<forall>m. Suc m\<le>n \<longrightarrow> (\<forall>t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>})"
@@ -1355,7 +1355,7 @@
 apply assumption (* wf_prog G *)
 done
 
-section "nested version"
+subsubsection "nested version"
 
 lemma nesting_lemma' [rule_format (no_asm)]: 
   assumes ax_derivs_asm: "\<And>A ts. ts \<subseteq> A \<Longrightarrow> P A ts" 
@@ -1425,7 +1425,7 @@
 done
 
 
-section "simultaneous version"
+subsubsection "simultaneous version"
 
 lemma MGF_simult_Methd_lemma: "finite ms \<Longrightarrow>  
   G,A \<union> (\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd  C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) ` ms  
@@ -1460,7 +1460,7 @@
 done
 
 
-section "corollaries"
+subsubsection "corollaries"
 
 lemma eval_to_evaln: "\<lbrakk>G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y', s');type_ok G t s; wf_prog G\<rbrakk>
  \<Longrightarrow>   \<exists>n. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')"
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/AxExample.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb
 *)
 
-header {* Example of a proof based on the Bali axiomatic semantics *}
+subsection {* Example of a proof based on the Bali axiomatic semantics *}
 
 theory AxExample
 imports AxSem Example
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/AxSem.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb
 *)
 
-header {* Axiomatic semantics of Java expressions and statements 
+subsection {* Axiomatic semantics of Java expressions and statements 
           (see also Eval.thy)
         *}
 theory AxSem imports Evaln TypeSafe begin
@@ -72,7 +72,7 @@
 done
 
 
-section "assertion transformers"
+subsubsection "assertion transformers"
 
 subsection "peek-and"
 
@@ -369,7 +369,7 @@
 apply (simp (no_asm))
 done
 
-section "validity"
+subsubsection "validity"
 
 definition
   type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where
@@ -644,7 +644,7 @@
   where "adapt_pre P Q Q' = (\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z))"
 
 
-section "rules derived by induction"
+subsubsection "rules derived by induction"
 
 lemma cut_valid: "\<lbrakk>G,A'|\<Turnstile>ts; G,A|\<Turnstile>A'\<rbrakk> \<Longrightarrow> G,A|\<Turnstile>ts"
 apply (unfold ax_valids_def)
@@ -715,7 +715,7 @@
 oops (* dead end, Methd is to blame *)
 
 
-section "rules derived from conseq"
+subsubsection "rules derived from conseq"
 
 text {* In the following rules we often have to give some type annotations like:
  @{term "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}"}.
@@ -914,7 +914,7 @@
 done
 
 
-section "alternative axioms"
+subsubsection "alternative axioms"
 
 lemma ax_Lit2: 
   "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} Lit v-\<succ> {Normal (P\<down>=Val v)}"
@@ -945,7 +945,7 @@
 done
 
 
-section "misc derived structural rules"
+subsubsection "misc derived structural rules"
 
 (* unused *)
 lemma ax_finite_mtriples_lemma: "\<lbrakk>F \<subseteq> ms; finite ms; \<forall>(C,sig)\<in>ms. 
@@ -1019,7 +1019,7 @@
 lemmas ax_SkipI = ax_Skip [THEN conseq1]
 
 
-section "derived rules for methd call"
+subsubsection "derived rules for methd call"
 
 lemma ax_Call_known_DynT: 
 "\<lbrakk>G\<turnstile>IntVir\<rightarrow>C\<preceq>statT; 
@@ -1084,7 +1084,7 @@
 apply clarsimp
 done
 
-section "rules derived from Init and Done"
+subsubsection "rules derived from Init and Done"
 
   lemma ax_InitS: "\<lbrakk>the (class G C) = c; C \<noteq> Object;  
      \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}  
@@ -1139,7 +1139,7 @@
 done
 
 
-section "introduction rules for Alloc and SXAlloc"
+subsubsection "introduction rules for Alloc and SXAlloc"
 
 lemma ax_SXAlloc_Normal: 
  "G,(A::'a triple set)\<turnstile>{P::'a assn} .c. {Normal Q} 
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/AxSound.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,13 +1,13 @@
 (*  Title:      HOL/Bali/AxSound.thy
     Author:     David von Oheimb and Norbert Schirmer
 *)
-header {* Soundness proof for Axiomatic semantics of Java expressions and 
+subsection {* Soundness proof for Axiomatic semantics of Java expressions and 
           statements
        *}
 
 theory AxSound imports AxSem begin
 
-section "validity"
+subsubsection "validity"
 
 definition
   triple_valid2 :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool"  ("_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
@@ -100,7 +100,7 @@
 oops
 
 
-section "soundness"
+subsubsection "soundness"
 
 lemma Methd_sound: 
   assumes recursive: "G,A\<union>  {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}"
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Basis.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,13 +1,13 @@
 (*  Title:      HOL/Bali/Basis.thy
     Author:     David von Oheimb
 *)
-header {* Definitions extending HOL as logical basis of Bali *}
+subsection {* Definitions extending HOL as logical basis of Bali *}
 
 theory Basis
 imports Main "~~/src/HOL/Library/Old_Recdef"
 begin
 
-section "misc"
+subsubsection "misc"
 
 ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *}
 
@@ -109,7 +109,7 @@
   done
 
 
-section "pairs"
+subsubsection "pairs"
 
 lemma surjective_pairing5:
   "p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))),
@@ -125,7 +125,7 @@
   by (induct l) auto
 
 
-section "quantifiers"
+subsubsection "quantifiers"
 
 lemma All_Ex_refl_eq2 [simp]: "(\<forall>x. (\<exists>b. x = f b \<and> Q b) \<longrightarrow> P x) = (\<forall>b. Q b \<longrightarrow> P (f b))"
   by auto
@@ -143,7 +143,7 @@
   by auto
 
 
-section "sums"
+subsubsection "sums"
 
 notation case_sum  (infixr "'(+')" 80)
 
@@ -186,7 +186,7 @@
 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
 
 
-section "quantifiers for option type"
+subsubsection "quantifiers for option type"
 
 syntax
   "_Oall" :: "[pttrn, 'a option, bool] \<Rightarrow> bool"   ("(3! _:_:/ _)" [0,0,10] 10)
@@ -201,7 +201,7 @@
   "\<exists>x\<in>A: P" \<rightleftharpoons> "\<exists>x\<in>CONST set_option A. P"
 
 
-section "Special map update"
+subsubsection "Special map update"
 
 text{* Deemed too special for theory Map. *}
 
@@ -218,7 +218,7 @@
   by (auto simp: chg_map_def)
 
 
-section "unique association lists"
+subsubsection "unique association lists"
 
 definition unique :: "('a \<times> 'b) list \<Rightarrow> bool"
   where "unique = distinct \<circ> map fst"
@@ -250,7 +250,7 @@
   by (induct l) auto
 
 
-section "list patterns"
+subsubsection "list patterns"
 
 definition lsplit :: "[['a, 'a list] \<Rightarrow> 'b, 'a list] \<Rightarrow> 'b"
   where "lsplit = (\<lambda>f l. f (hd l) (tl l))"
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/Conform.thy
--- a/src/HOL/Bali/Conform.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Conform.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb
 *)
 
-header {* Conformance notions for the type soundness proof for Java *}
+subsection {* Conformance notions for the type soundness proof for Java *}
 
 theory Conform imports State begin
 
@@ -19,7 +19,7 @@
 type_synonym env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
 
 
-section "extension of global store"
+subsubsection "extension of global store"
 
 
 definition gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>|_"       [71,71]   70) where
@@ -94,7 +94,7 @@
 done
 
 
-section "value conformance"
+subsubsection "value conformance"
 
 definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
   where "G,s\<turnstile>v\<Colon>\<preceq>T = (\<exists>T'\<in>typeof (\<lambda>a. map_option obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T)"
@@ -175,7 +175,7 @@
 done
 
 
-section "value list conformance"
+subsubsection "value list conformance"
 
 definition
   lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
@@ -248,7 +248,7 @@
 apply force
 done
 
-section "weak value list conformance"
+subsubsection "weak value list conformance"
 
 text {* Only if the value is defined it has to conform to its type. 
         This is the contribution of the definite assignment analysis to 
@@ -338,7 +338,7 @@
  "G,s\<turnstile>l[\<Colon>\<preceq>]L \<Longrightarrow> G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
 by (force simp add: lconf_def wlconf_def)
 
-section "object conformance"
+subsubsection "object conformance"
 
 definition
   oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70) where
@@ -373,7 +373,7 @@
 apply (auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm)
 done
 
-section "state conformance"
+subsubsection "state conformance"
 
 definition
   conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"  ("_\<Colon>\<preceq>_" [71,71] 70)  where
@@ -383,7 +383,7 @@
         (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
              (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None))"
 
-section "conforms"
+subsubsection "conforms"
 
 lemma conforms_globsD: 
 "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some obj\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Decl.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Decl.thy
     Author:     David von Oheimb and Norbert Schirmer
 *)
-header {* Field, method, interface, and class declarations, whole Java programs
+subsection {* Field, method, interface, and class declarations, whole Java programs
 *}
 
 theory Decl
@@ -367,7 +367,7 @@
 by (simp add: cbody_def)
 
 
-section "standard classes"
+subsubsection "standard classes"
 
 consts
   Object_mdecls  ::  "mdecl list" --{* methods of Object *}
@@ -399,7 +399,7 @@
                 SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
 
 
-section "programs"
+subsubsection "programs"
 
 record prog =
         ifaces ::"idecl list"
@@ -426,7 +426,7 @@
   where "is_class G C == class G C \<noteq> None"
 
 
-section "is type"
+subsubsection "is type"
 
 primrec is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
   and isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
@@ -445,7 +445,7 @@
 by auto
 
 
-section "subinterface and subclass relation, in anticipation of TypeRel.thy"
+subsubsection "subinterface and subclass relation, in anticipation of TypeRel.thy"
 
 definition
   subint1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subinterface *}
@@ -516,7 +516,7 @@
 apply (auto intro: no_subcls1_Object)
 done
 
-section "well-structured programs"
+subsubsection "well-structured programs"
 
 definition
   ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool"
@@ -562,7 +562,7 @@
 done
 
 
-section "well-foundedness"
+subsubsection "well-foundedness"
 
 lemma finite_is_iface: "finite {I. is_iface G I}"
 apply (fold dom_def)
@@ -765,7 +765,7 @@
   qed
 qed
 
-section "general recursion operators for the interface and class hiearchies"
+subsubsection "general recursion operators for the interface and class hiearchies"
 
 function iface_rec  :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
 where
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,12 +1,12 @@
 (*  Title:      HOL/Bali/DeclConcepts.thy
     Author:     Norbert Schirmer
 *)
-header {* Advanced concepts on Java declarations like overriding, inheritance,
+subsection {* Advanced concepts on Java declarations like overriding, inheritance,
 dynamic method lookup*}
 
 theory DeclConcepts imports TypeRel begin
 
-section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
+subsubsection "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
 
 definition is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool" where
 "is_public G qn = (case class G qn of
@@ -1389,7 +1389,7 @@
   qed
 qed
 
-section "fields and methods"
+subsubsection "fields and methods"
 
 
 type_synonym
@@ -2282,7 +2282,7 @@
 apply assumption
 done
 
-section "calculation of the superclasses of a class"
+subsubsection "calculation of the superclasses of a class"
 
 definition
   superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/DefiniteAssignment.thy
--- 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" 
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,4 +1,4 @@
-header {* Correctness of Definite Assignment *}
+subsection {* Correctness of Definite Assignment *}
 
 theory DefiniteAssignmentCorrect imports WellForm Eval begin
 
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Eval.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Eval.thy
     Author:     David von Oheimb
 *)
-header {* Operational evaluation (big-step) semantics of Java expressions and 
+subsection {* Operational evaluation (big-step) semantics of Java expressions and 
           statements
 *}
 
@@ -157,7 +157,7 @@
 by (simp add: undefined3_def)
 
 
-section "exception throwing and catching"
+subsubsection "exception throwing and catching"
 
 definition
   throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" where
@@ -233,7 +233,7 @@
 
 
 
-section "misc"
+subsubsection "misc"
 
 definition
   assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where
@@ -385,7 +385,7 @@
 apply auto
 done
 
-section "variables"
+subsubsection "variables"
 
 definition
   lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
@@ -467,7 +467,7 @@
                   AccessViolation)
         s)"
        
-section "evaluation judgments"
+subsubsection "evaluation judgments"
 
 inductive
   halloc :: "[prog,state,obj_tag,loc,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60) for G::prog
@@ -1123,7 +1123,7 @@
 qed
 
 
-section "single valued"
+subsubsection "single valued"
 
 lemma unique_halloc [rule_format (no_asm)]: 
   "G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>halloc oi\<succ>a' \<rightarrow> s'' \<longrightarrow> a' = a \<and> s'' = s'"
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Evaln.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Evaln.thy
     Author:     David von Oheimb and Norbert Schirmer
 *)
-header {* Operational evaluation (big-step) semantics of Java expressions and 
+subsection {* Operational evaluation (big-step) semantics of Java expressions and 
           statements
 *}
 
@@ -401,7 +401,7 @@
 
 
 
-section {* evaln implies eval *}
+subsubsection {* evaln implies eval *}
 
 lemma evaln_eval:  
   assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" 
@@ -510,7 +510,7 @@
 
 declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
 
-section {* eval implies evaln *}
+subsubsection {* eval implies evaln *}
 lemma eval_evaln: 
   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Example.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Example.thy
     Author:     David von Oheimb
 *)
-header {* Example Bali program *}
+subsection {* Example Bali program *}
 
 theory Example
 imports Eval WellForm
@@ -63,7 +63,7 @@
 declare wf_fdecl_def2 [iff]
 
 
-section "type and expression names"
+subsubsection "type and expression names"
 
 (** unfortunately cannot simply instantiate tnam **)
 datatype tnam'  = HasFoo' | Base' | Ext' | Main'
@@ -141,7 +141,7 @@
 lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
 by (simp add: SXcpt_def)
 
-section "classes and interfaces"
+subsubsection "classes and interfaces"
 
 defs
 
@@ -266,7 +266,7 @@
 apply (simp (no_asm) add: Object_def SXcpt_def)
 done
 
-section "program"
+subsubsection "program"
 
 abbreviation
   tprg :: prog where
@@ -281,7 +281,7 @@
                         (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip))"
 
 
-section "well-structuredness"
+subsubsection "well-structuredness"
 
 lemma not_Object_subcls_any [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
 apply (auto dest!: tranclD subcls1D)
@@ -378,7 +378,7 @@
 done
 
 
-section "misc program properties (independent of well-structuredness)"
+subsubsection "misc program properties (independent of well-structuredness)"
 
 lemma single_iface [simp]: "is_iface tprg I = (I = HasFoo)"
 apply (unfold Ifaces_def)
@@ -421,7 +421,7 @@
 
 
 
-section "fields and method lookup"
+subsubsection "fields and method lookup"
 
 lemma fields_tprg_Object [simp]: "DeclConcepts.fields tprg Object = []"
 by (rule ws_tprg [THEN fields_emptyI], force+)
@@ -531,7 +531,7 @@
 apply   (auto simp add: ExtCl_def Object_def Ext_method_inheritance)
 done
 
-section "accessibility"
+subsubsection "accessibility"
 
 lemma classesDefined: 
  "\<lbrakk>class tprg C = Some c; C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class tprg (super c) = Some sc"
@@ -881,7 +881,7 @@
 done
 
 
-section "well-formedness"
+subsubsection "well-formedness"
 
 
 lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)"
@@ -1059,7 +1059,7 @@
 apply  auto
 done
 
-section "max spec"
+subsubsection "max spec"
 
 lemma appl_methds_Base_foo: 
 "appl_methds tprg S (ClassT Base) \<lparr>name=foo, parTs=[NT]\<rparr> =  
@@ -1076,7 +1076,7 @@
    , [Class Base])}"
 by (simp add: max_spec_def appl_methds_Base_foo Collect_conv_if)
 
-section "well-typedness"
+subsubsection "well-typedness"
 
 schematic_lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
 apply (unfold test_def arr_viewed_from_def)
@@ -1128,7 +1128,7 @@
 apply (rule wtIs (* Skip *))
 done
 
-section "definite assignment"
+subsubsection "definite assignment"
 
 schematic_lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
                   \<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
@@ -1171,7 +1171,7 @@
 done
 
 
-section "execution"
+subsubsection "execution"
 
 lemma alloc_one: "\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow>  
   new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n"
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/Name.thy
--- a/src/HOL/Bali/Name.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Name.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Name.thy
     Author:     David von Oheimb
 *)
-header {* Java names *}
+subsection {* Java names *}
 
 theory Name imports Basis begin
 
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/State.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/State.thy
     Author:     David von Oheimb
 *)
-header {* State for evaluation of Java expressions and statements *}
+subsection {* State for evaluation of Java expressions and statements *}
 
 theory State
 imports DeclConcepts
@@ -17,7 +17,7 @@
 \end{itemize}
 *}
 
-section "objects"
+subsubsection "objects"
 
 datatype  obj_tag =     --{* tag for generic object   *}
           CInst qtname  --{* class instance           *}
@@ -128,7 +128,7 @@
 apply (auto dest: widen_Array_Class)
 done
 
-section "object references"
+subsubsection "object references"
 
 type_synonym oref = "loc + qtname"         --{* generalized object reference *}
 syntax
@@ -211,7 +211,7 @@
 done
 
 
-section "stores"
+subsubsection "stores"
 
 type_synonym globs               --{* global variables: heap and static variables *}
         = "(oref , obj) table"
@@ -459,7 +459,7 @@
 done
 
 
-section "abrupt completion"
+subsubsection "abrupt completion"
 
 
 
@@ -577,7 +577,7 @@
   by (simp add: absorb_def)
 
 
-section "full program state"
+subsubsection "full program state"
 
 type_synonym
   state = "abopt \<times> st"          --{* state including abruption information *}
@@ -687,7 +687,7 @@
 apply (simp (no_asm))
 done
 
-section "initialisation test"
+subsubsection "initialisation test"
 
 definition
   inited :: "qtname \<Rightarrow> globs \<Rightarrow> bool"
@@ -727,7 +727,7 @@
 apply (simp (no_asm))
 done
 
-section {* @{text error_free} *}
+subsubsection {* @{text error_free} *}
 
 definition
   error_free :: "state \<Rightarrow> bool"
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"
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Term.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb
 *)
 
-header {* Java expressions and statements *}
+subsection {* Java expressions and statements *}
 
 theory Term imports Value Table begin
 
@@ -427,7 +427,7 @@
   apply auto
   done
 
-section {* Evaluation of unary operations *}
+subsubsection {* Evaluation of unary operations *}
 primrec eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
 where
   "eval_unop UPlus v = Intg (the_Intg v)"
@@ -435,7 +435,7 @@
 | "eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
 | "eval_unop UNot v = Bool (\<not> the_Bool v)"
 
-section {* Evaluation of binary operations *}
+subsubsection {* Evaluation of binary operations *}
 primrec eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
 where
   "eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/Type.thy
--- a/src/HOL/Bali/Type.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Type.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb
 *)
 
-header {* Java types *}
+subsection {* Java types *}
 
 theory Type imports Name begin
 
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/TypeRel.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/TypeRel.thy
     Author:     David von Oheimb
 *)
-header {* The relations between Java types *}
+subsection {* The relations between Java types *}
 
 theory TypeRel imports Decl begin
 
@@ -55,7 +55,7 @@
   implmt1_syntax   ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
 
 
-section "subclass and subinterface relations"
+subsubsection "subclass and subinterface relations"
 
   (* direct subinterface in Decl.thy, cf. 9.1.3 *)
   (* direct subclass     in Decl.thy, cf. 8.1.3 *)
@@ -327,7 +327,7 @@
   qed
 qed
 
-section "implementation relation"
+subsubsection "implementation relation"
 
 lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"
 apply (unfold implmt1_def)
@@ -366,7 +366,7 @@
 done
 
 
-section "widening relation"
+subsubsection "widening relation"
 
 inductive
  --{*widening, viz. method invocation conversion, cf. 5.3
@@ -583,7 +583,7 @@
 done
 
 
-section "narrowing relation"
+subsubsection "narrowing relation"
 
 (* all properties of narrowing and casting conversions we actually need *)
 (* these can easily be proven from the definitions below *)
@@ -643,7 +643,7 @@
 lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean"
 by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean")
 
-section "casting relation"
+subsubsection "casting relation"
 
 inductive --{* casting conversion, cf. 5.5 *}
   cast :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,13 +1,13 @@
 (*  Title:      HOL/Bali/TypeSafe.thy
     Author:     David von Oheimb and Norbert Schirmer
 *)
-header {* The type soundness proof for Java *}
+subsection {* The type soundness proof for Java *}
 
 theory TypeSafe
 imports DefiniteAssignmentCorrect Conform
 begin
 
-section "error free"
+subsubsection "error free"
  
 lemma error_free_halloc:
   assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
@@ -90,7 +90,7 @@
 by (cases s) (simp add: throw_def)
 
 
-section "result conformance"
+subsubsection "result conformance"
 
 definition
   assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool" ("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70)
@@ -163,7 +163,7 @@
 apply (simp (no_asm))
 done
 
-section "fits and conf"
+subsubsection "fits and conf"
 
 (* unused *)
 lemma conf_fits: "G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T"
@@ -188,7 +188,7 @@
 
 
 
-section "gext"
+subsubsection "gext"
 
 lemma halloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
 apply (simp (no_asm_simp) only: split_tupled_all)
@@ -242,7 +242,7 @@
 done
 
 
-section "Lemmas"
+subsubsection "Lemmas"
 
 lemma obj_ty_obj_class1: 
  "\<lbrakk>wf_prog G; is_type G (obj_ty obj)\<rbrakk> \<Longrightarrow> is_class G (obj_class obj)"
@@ -809,7 +809,7 @@
 done
 
 
-section "Call"
+subsubsection "Call"
 
 lemma conforms_init_lvars_lemma: "\<lbrakk>wf_prog G;  
   wf_mhead G P sig mh;
@@ -1699,7 +1699,7 @@
   thus ?thesis ..
 qed
 
-section "main proof of type safety"
+subsubsection "main proof of type safety"
     
 lemma eval_type_sound:
   assumes  eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/Value.thy
--- a/src/HOL/Bali/Value.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/Value.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Value.thy
     Author:     David von Oheimb
 *)
-header {* Java values *}
+subsection {* Java values *}
 
 
 
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/WellForm.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb and Norbert Schirmer
 *)
 
-header {* Well-formedness of Java programs *}
+subsection {* Well-formedness of Java programs *}
 theory WellForm imports DefiniteAssignment begin
 
 text {*
@@ -27,7 +27,7 @@
 \end{itemize}
 *}
 
-section "well-formed field declarations"
+subsubsection "well-formed field declarations"
 text  {* well-formed field declaration (common part for classes and interfaces),
         cf. 8.3 and (9.3) *}
 
@@ -42,7 +42,7 @@
 
 
 
-section "well-formed method declarations"
+subsubsection "well-formed method declarations"
   (*well-formed method declaration,cf. 8.4, 8.4.1, 8.4.3, 8.4.5, 14.3.2, (9.4)*)
   (* cf. 14.15, 15.7.2, for scope issues cf. 8.4.1 and 14.3.2 *)
 
@@ -202,7 +202,7 @@
 apply auto
 done
 
-section "well-formed interface declarations"
+subsubsection "well-formed interface declarations"
   (* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *)
 
 text {*
@@ -273,7 +273,7 @@
 apply auto
 done
 
-section "well-formed class declarations"
+subsubsection "well-formed class declarations"
   (* well-formed class declaration, cf. 8.1, 8.1.2.1, 8.1.2.2, 8.1.3, 8.1.4 and
    class method declaration, cf. 8.4.3.3, 8.4.6.1, 8.4.6.2, 8.4.6.3, 8.4.6.4 *)
 
@@ -500,7 +500,7 @@
 done
 
 
-section "well-formed programs"
+subsubsection "well-formed programs"
   (* well-formed program, cf. 8.1, 9.1 *)
 
 text {*
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/WellType.thy	Sun Nov 02 18:16:19 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/WellType.thy
     Author:     David von Oheimb
 *)
-header {* Well-typedness of Java programs *}
+subsection {* Well-typedness of Java programs *}
 
 theory WellType
 imports DeclConcepts
@@ -47,7 +47,7 @@
   pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
   where "pkg e == pid (cls e)"
 
-section "Static overloading: maximally specific methods "
+subsubsection "Static overloading: maximally specific methods "
 
 type_synonym
   emhead = "ref_ty \<times> mhead"
@@ -174,7 +174,7 @@
 apply (clarsimp simp add: invmode_IntVir_eq)
 done
 
-section "Typing for unary operations"
+subsubsection "Typing for unary operations"
 
 primrec unop_type :: "unop \<Rightarrow> prim_ty"
 where
@@ -190,7 +190,7 @@
 | "wt_unop UBitNot t = (t = PrimT Integer)"
 | "wt_unop UNot    t = (t = PrimT Boolean)"
 
-section "Typing for binary operations"
+subsubsection "Typing for binary operations"
 
 primrec binop_type :: "binop \<Rightarrow> prim_ty"
 where
@@ -242,7 +242,7 @@
 | "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
 | "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
 
-section "Typing for terms"
+subsubsection "Typing for terms"
 
 type_synonym tys  = "ty + ty list"
 translations
diff -r 8a6cac7c7247 -r 38db8ddc0f57 src/HOL/Bali/document/root.tex
--- a/src/HOL/Bali/document/root.tex	Sun Nov 02 17:58:35 2014 +0100
+++ b/src/HOL/Bali/document/root.tex	Sun Nov 02 18:16:19 2014 +0100
@@ -19,8 +19,7 @@
 
 %subsection instead of section to make the toc readable
 \renewcommand{\thesubsection}{\arabic{subsection}}
-\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
-\renewcommand{\isamarkupsection}[1]{\subsubsection{#1}}
+\renewcommand{\setisabellecontext}[1]{\markright{Theory~#1}}
 
 %remove spaces from the isabelle environment (trivlist makes them too large)
 \renewenvironment{isabelle}