# HG changeset patch
# User wenzelm
# Date 1414947515 -3600
# Node ID 8a6cac7c724741666647fd17afe4747bc4688098
# Parent  47fdd4f40d00c215f490606400f5ed1db1f90052
modernized header;

diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/Altern.thy
--- a/src/HOL/MicroJava/BV/Altern.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/Altern.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Martin Strecker
 *)
 
-header {* Alternative definition of well-typing of bytecode,  used in compiler type correctness proof *}
+section {* Alternative definition of well-typing of bytecode,  used in compiler type correctness proof *}
 
 theory Altern
 imports BVSpec
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Gerwin Klein
 *)
 
-header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
+section {* Example Welltypings \label{sec:BVExample} *}
 
 theory BVExample
 imports
@@ -19,7 +19,7 @@
   execution is guaranteed.
 *}
 
-section "Setup"
+subsection "Setup"
 
 text {* Abbreviations for definitions we will have to use often in the
 proofs below: *}
@@ -178,7 +178,7 @@
   by (unfold intervall_def) arith
 
 
-section "Program structure"
+subsection "Program structure"
 
 text {*
   The program is structurally wellformed:
@@ -225,7 +225,7 @@
     by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def)
 qed
 
-section "Welltypings"
+subsection "Welltypings"
 text {*
   We show welltypings of the methods @{term append_name} in class @{term list_name}, 
   and @{term makelist_name} in class @{term test_name}:
@@ -385,7 +385,7 @@
   done 
 
 
-section "Conformance"
+subsection "Conformance"
 text {* Execution of the program will be typesafe, because its
   start state conforms to the welltyping: *}
 
@@ -397,7 +397,7 @@
   done
 
 
-section "Example for code generation: inferring method types"
+subsection "Example for code generation: inferring method types"
 
 definition test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
              exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state list" where
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Gerwin Klein
 *)
 
-header {* \isaheader{Welltyped Programs produce no Type Errors} *}
+section {* Welltyped Programs produce no Type Errors *}
 
 theory BVNoTypeError
 imports "../JVM/JVMDefensive" BVSpecTypeSafe
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{The Bytecode Verifier}\label{sec:BVSpec} *}
+section {* The Bytecode Verifier \label{sec:BVSpec} *}
 
 theory BVSpec
 imports Effect
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *}
+section {* BV Type Safety Proof \label{sec:BVSpecTypeSafe} *}
 
 theory BVSpecTypeSafe
 imports Correct
@@ -14,7 +14,7 @@
   verifier only admits type safe programs.  
 *}
 
-section {* Preliminaries *}
+subsection {* Preliminaries *}
 
 text {*
   Simp and intro setup for the type safety proof:
@@ -41,7 +41,7 @@
 done
 
 
-section {* Exception Handling *}
+subsection {* Exception Handling *}
 
 text {*
   Exceptions don't touch anything except the stack:
@@ -582,7 +582,7 @@
 
 
 
-section {* Single Instructions *}
+subsection {* Single Instructions *}
 
 text {*
   In this section we look at each single (welltyped) instruction, and
@@ -1265,7 +1265,7 @@
 apply (rule Throw_correct, assumption+)
 done
 
-section {* Main *}
+subsection {* Main *}
 
 lemma correct_state_impl_Some_method:
   "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{BV Type Safety Invariant} *}
+section {* BV Type Safety Invariant *}
 
 theory Correct
 imports BVSpec "../JVM/JVMExec"
@@ -68,7 +68,7 @@
   by (cases X) auto
 
 
-section {* approx-val *}
+subsection {* approx-val *}
 
 lemma approx_val_Err [simp,intro!]:
   "approx_val G hp x Err"
@@ -96,7 +96,7 @@
   \<Longrightarrow> approx_val G hp v T'"
   by (cases T') (auto simp add: sup_ty_opt_OK intro: conf_widen)
 
-section {* approx-loc *}
+subsection {* approx-loc *}
 
 lemma approx_loc_Nil [simp,intro!]:
   "approx_loc G hp [] []"
@@ -170,7 +170,7 @@
   apply blast
   done
 
-section {* approx-stk *}
+subsection {* approx-stk *}
 
 lemma approx_stk_rev_lem:
   "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
@@ -221,7 +221,7 @@
 apply (erule conf_widen, assumption+)
 done
 
-section {* oconf *}
+subsection {* oconf *}
 
 lemma oconf_field_update:
   "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
@@ -242,7 +242,7 @@
   apply (fastforce intro: approx_val_heap_update)
   done
 
-section {* hconf *}
+subsection {* hconf *}
 
 lemma hconf_newref:
   "\<lbrakk> hp oref = None; G\<turnstile>h hp\<surd>; G,hp\<turnstile>obj\<surd> \<rbrakk> \<Longrightarrow> G\<turnstile>h hp(oref\<mapsto>obj)\<surd>"
@@ -259,7 +259,7 @@
                   simp add: obj_ty_def)
   done
 
-section {* preallocated *}
+subsection {* preallocated *}
 
 lemma preallocated_field_update:
   "\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); 
@@ -289,7 +289,7 @@
   with alloc show ?thesis by (simp add: preallocated_def)
 qed
   
-section {* correct-frames *}
+subsection {* correct-frames *}
 
 lemmas [simp del] = fun_upd_apply
 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Effect of Instructions on the State Type} *}
+section {* Effect of Instructions on the State Type *}
 
 theory Effect 
 imports JVMType "../JVM/JVMExceptions"
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Monotonicity of eff and app} *}
+section {* Monotonicity of eff and app *}
 
 theory EffectMono
 imports Effect
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/JType.thy
--- a/src/HOL/MicroJava/BV/JType.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-header {* \isaheader{The Java Type System as Semilattice} *}
+section {* The Java Type System as Semilattice *}
 
 theory JType
 imports "../DFA/Semilattices" "../J/WellForm"
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
+section {* Kildall for the JVM \label{sec:JVM} *}
 
 theory JVM
 imports Typing_Framework_JVM
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-header {* \isaheader{The JVM Type System as Semilattice} *}
+section {* The JVM Type System as Semilattice *}
 
 theory JVMType
 imports JType
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/LBVJVM.thy
--- a/src/HOL/MicroJava/BV/LBVJVM.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-header {* \isaheader{LBV for the JVM}\label{sec:JVM} *}
+section {* LBV for the JVM \label{sec:JVM} *}
 
 theory LBVJVM
 imports Typing_Framework_JVM
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *}
+section {* The Typing Framework for the JVM \label{sec:JVM} *}
 
 theory Typing_Framework_JVM
 imports "../DFA/Abstract_BV" JVMType EffectMono BVSpec
@@ -17,7 +17,7 @@
   "opt_states G maxs maxr \<equiv> opt (\<Union>{list n (types G) |n. n \<le> maxs} \<times> list maxr (err (types G)))"
 
 
-section {*  Executability of @{term check_bounded} *}
+subsection {*  Executability of @{term check_bounded} *}
 
 primrec list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
 where
@@ -46,7 +46,7 @@
   by (simp add: list_all_iff check_bounded_def)
   
 
-section {* Connecting JVM and Framework *}
+subsection {* Connecting JVM and Framework *}
 
 lemma check_bounded_is_bounded:
   "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"  
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -37,7 +37,7 @@
 
 
 (********************************************************************************)
-section "index"
+subsection "index"
 
 lemma local_env_snd: "
   snd (local_env G C (mn, pTs) pns lvars) = map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)"
@@ -195,7 +195,7 @@
 
 (********************************************************************************)
 
-section "Preservation of ST and LT by compTpExpr / compTpStmt"
+subsection "Preservation of ST and LT by compTpExpr / compTpStmt"
 
 lemma sttp_of_comb_nil [simp]: "sttp_of (comb_nil sttp) = sttp"
 by (simp add: comb_nil_def)
@@ -787,7 +787,7 @@
 
 
   (* ********************************************************************** *)
-section "length of compExpr/ compTpExprs"
+subsection "length of compExpr/ compTpExprs"
   (* ********************************************************************** *)
 
 lemma length_comb [simp]:  "length (mt_of ((f1 \<box> f2) sttp)) = 
@@ -853,7 +853,7 @@
 
 
   (* ********************************************************************** *)
-section "Correspondence bytecode - method types"
+subsection "Correspondence bytecode - method types"
   (* ********************************************************************** *)
 
 abbreviation (input)
@@ -2559,7 +2559,7 @@
 
   (* ---------------------------------------------------------------------- *)
 
-section "Main Theorem"
+subsection "Main Theorem"
   (* MAIN THEOREM: 
   Methodtype computed by comp is correct for bytecode generated by compTp *)
 theorem wt_prog_comp: "wf_java_prog G  \<Longrightarrow> wt_jvm_prog (comp G) (compTp G)"
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/Abstract_BV.thy
--- a/src/HOL/MicroJava/DFA/Abstract_BV.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Abstract_BV.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2003 TUM
 *)
 
-header {* Abstract Bytecode Verifier *}
+section {* Abstract Bytecode Verifier *}
 
 (*<*)
 theory Abstract_BV
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/Err.thy
--- a/src/HOL/MicroJava/DFA/Err.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Err.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-header {* \isaheader{The Error Type} *}
+section {* The Error Type *}
 
 theory Err
 imports Semilat
@@ -166,7 +166,7 @@
 lemma Ok_in_err [iff]: "(OK x : err A) = (x:A)"
   by (auto simp add: err_def)
 
-section {* lift *}
+subsection {* lift *}
 
 lemma lift_in_errI:
   "\<lbrakk> e : err S; !x:S. e = OK x \<longrightarrow> f x : err S \<rbrakk> \<Longrightarrow> lift f e : err S"
@@ -188,7 +188,7 @@
   by (simp add: lift2_def plussub_def split: err.split)
 
 
-section {* sup *}
+subsection {* sup *}
 
 lemma Err_sup_Err [simp]:
   "Err +_(Err.sup f) x = Err"
@@ -217,7 +217,7 @@
 apply (simp split: err.split)
 done 
 
-section {* semilat (err A) (le r) f *}
+subsection {* semilat (err A) (le r) f *}
 
 lemma semilat_le_err_Err_plus [simp]:
   "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> Err +_f x = Err"
@@ -283,7 +283,7 @@
   done 
 qed
 
-section {* semilat (err(Union AS)) *}
+subsection {* semilat (err(Union AS)) *}
 
 (* FIXME? *)
 lemma all_bex_swap_lemma [iff]:
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
+section {* Kildall's Algorithm \label{sec:Kildall} *}
 
 theory Kildall
 imports SemilatAlg "~~/src/HOL/Library/While_Combinator"
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/LBVComplete.thy
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Completeness of the LBV} *}
+section {* Completeness of the LBV *}
 
 theory LBVComplete
 imports LBVSpec Typing_Framework
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/LBVCorrect.thy
--- a/src/HOL/MicroJava/DFA/LBVCorrect.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/LBVCorrect.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Correctness of the LBV} *}
+section {* Correctness of the LBV *}
 
 theory LBVCorrect
 imports LBVSpec Typing_Framework
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/LBVSpec.thy
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{The Lightweight Bytecode Verifier} *}
+section {* The Lightweight Bytecode Verifier *}
 
 theory LBVSpec
 imports SemilatAlg Opt
@@ -92,7 +92,7 @@
 
 declare Let_def [simp]
 
-section "more semilattice lemmas"
+subsection "more semilattice lemmas"
 
 
 lemma (in lbv) sup_top [simp, elim]:
@@ -129,7 +129,7 @@
 
 
 
-section "merge"
+subsection "merge"
 
 lemma (in lbv) merge_Nil [simp]:
   "merge c pc [] x = x" by (simp add: mrg_def)
@@ -226,7 +226,7 @@
   with x ss m show ?thesis by - (drule merge_def, auto split: split_if_asm)
 qed
 
-section "wtl-inst-list"
+subsection "wtl-inst-list"
 
 lemmas [iff] = not_Err_eq
 
@@ -301,7 +301,7 @@
   with take pc show ?thesis by (auto simp add: min.absorb2)
 qed
 
-section "preserves-type"
+subsection "preserves-type"
 
 lemma (in lbv) merge_pres:
   assumes s0: "snd`set ss \<subseteq> A" and x: "x \<in> A"
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/Listn.thy
--- a/src/HOL/MicroJava/DFA/Listn.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Listn.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-header {* \isaheader{Fixed Length Lists} *}
+section {* Fixed Length Lists *}
 
 theory Listn
 imports Err
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/Opt.thy
--- a/src/HOL/MicroJava/DFA/Opt.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Opt.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-header {* \isaheader{More about Options} *}
+section {* More about Options *}
 
 theory Opt
 imports Err
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/Product.thy
--- a/src/HOL/MicroJava/DFA/Product.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Product.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-header {* \isaheader{Products as Semilattices} *}
+section {* Products as Semilattices *}
 
 theory Product
 imports Err
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,10 +3,9 @@
     Copyright   2000 TUM
 *)
 
-header {* 
-  \chapter{Bytecode Verifier}\label{cha:bv}
-  \isaheader{Semilattices} 
-*}
+chapter {* Bytecode Verifier \label{cha:bv} *}
+
+section {* Semilattices *}
 
 theory Semilat
 imports Main "~~/src/HOL/Library/While_Combinator"
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/SemilatAlg.thy
--- a/src/HOL/MicroJava/DFA/SemilatAlg.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2002 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{More on Semilattices} *}
+section {* More on Semilattices *}
 
 theory SemilatAlg
 imports Typing_Framework Product
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/Semilattices.thy
--- a/src/HOL/MicroJava/DFA/Semilattices.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Semilattices.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2003 TUM
 *)
 
-header {* Semilattices *}
+section {* Semilattices *}
 
 (*<*)
 theory Semilattices
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/Typing_Framework.thy
--- a/src/HOL/MicroJava/DFA/Typing_Framework.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Typing_Framework.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-header {* \isaheader{Typing and Dataflow Analysis Framework} *}
+section {* Typing and Dataflow Analysis Framework *}
 
 theory Typing_Framework
 imports Listn
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/DFA/Typing_Framework_err.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Typing_Framework_err.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2000 TUM
 *)
 
-header {* \isaheader{Lifting the Typing Framework to err, app, and eff} *}
+section {* Lifting the Typing Framework to err, app, and eff *}
 
 theory Typing_Framework_err
 imports Typing_Framework SemilatAlg
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Conformity Relations for Type Soundness Proof} *}
+section {* Conformity Relations for Type Soundness Proof *}
 
 theory Conform imports State WellType Exceptions begin
 
@@ -44,7 +44,7 @@
   conforms  ("_ ::\<preceq> _" [51,51] 50)
 
 
-section "hext"
+subsection "hext"
 
 lemma hextI: 
 " \<forall>a C fs . h  a = Some (C,fs) -->   
@@ -79,7 +79,7 @@
 done
 
 
-section "conf"
+subsection "conf"
 
 lemma conf_Null [simp]: "G,h\<turnstile>Null::\<preceq>T = G\<turnstile>RefT NullT\<preceq>T"
 apply (unfold conf_def)
@@ -182,7 +182,7 @@
 done
 
 
-section "lconf"
+subsection "lconf"
 
 lemma lconfD: "[| G,h\<turnstile>vs[::\<preceq>]Ts; Ts n = Some T |] ==> G,h\<turnstile>(the (vs n))::\<preceq>T"
 apply (unfold lconf_def)
@@ -242,7 +242,7 @@
 apply auto
 done
 
-section "oconf"
+subsection "oconf"
 
 lemma oconf_hext: "G,h\<turnstile>obj\<surd> ==> h\<le>|h' ==> G,h'\<turnstile>obj\<surd>"
 apply (unfold oconf_def)
@@ -258,7 +258,7 @@
 lemmas oconf_objD = oconf_obj [THEN iffD1, THEN spec, THEN spec, THEN mp]
 
 
-section "hconf"
+subsection "hconf"
 
 lemma hconfD: "[|G\<turnstile>h h\<surd>; h a = Some obj|] ==> G,h\<turnstile>obj\<surd>"
 apply (unfold hconf_def)
@@ -271,14 +271,14 @@
 done
 
 
-section "xconf"
+subsection "xconf"
 
 lemma xconf_raise_if: "xconf h x \<Longrightarrow> xconf h (raise_if b xcn x)"
 by (simp add: xconf_def raise_if_def)
 
 
 
-section "conforms"
+subsection "conforms"
 
 lemma conforms_heapD: "(x, (h, l))::\<preceq>(G, lT) ==> G\<turnstile>h h\<surd>"
 apply (unfold conforms_def)
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Class Declarations and Programs} *}
+section {* Class Declarations and Programs *}
 
 theory Decl imports Type begin
 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Operational Evaluation (big step) Semantics} *}
+section {* Operational Evaluation (big step) Semantics *}
 
 theory Eval imports State WellType begin
 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Example MicroJava Program} *}
+section {* Example MicroJava Program *}
 
 theory Example imports SystemClasses Eval begin
 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/JBasis.thy
--- a/src/HOL/MicroJava/J/JBasis.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,16 +2,15 @@
     Author:     David von Oheimb, TU Muenchen
 *)
 
-header {* 
-  \chapter{Java Source Language}\label{cha:j}
-  \isaheader{Some Auxiliary Definitions}
-*}
+chapter {* Java Source Language \label{cha:j} *}
+
+section {* Some Auxiliary Definitions *}
 
 theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin 
 
 lemmas [simp] = Let_def
 
-section "unique"
+subsection "unique"
  
 definition unique :: "('a \<times> 'b) list => bool" where
   "unique == distinct \<circ> map fst"
@@ -34,7 +33,7 @@
   by (induct l) (auto dest: fst_in_set_lemma simp add: inj_eq)
 
 
-section "More about Maps"
+subsection "More about Maps"
 
 lemma map_of_SomeI: "unique l ==> (k, x) : set l ==> map_of l k = Some x"
   by (induct l) auto
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Stefan Berghofer
 *)
 
-header {* \isaheader{Example for generating executable code from Java semantics} *}
+section {* Example for generating executable code from Java semantics *}
 
 theory JListExample
 imports Eval
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Type Safety Proof} *}
+section {* Type Safety Proof *}
 
 theory JTypeSafe imports Eval Conform begin
 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/State.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Program State} *}
+section {* Program State *}
 
 theory State
 imports TypeRel Value
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/SystemClasses.thy
--- a/src/HOL/MicroJava/J/SystemClasses.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/SystemClasses.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2002 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{System Classes} *}
+section {* System Classes *}
 
 theory SystemClasses imports Decl begin
 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Term.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Expressions and Statements} *}
+section {* Expressions and Statements *}
 
 theory Term imports Value begin
 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/Type.thy
--- a/src/HOL/MicroJava/J/Type.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Type.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Java types} *}
+section {* Java types *}
 
 theory Type imports JBasis begin
 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Relations between Java Types} *}
+section {* Relations between Java Types *}
 
 theory TypeRel
 imports Decl
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/Value.thy
--- a/src/HOL/MicroJava/J/Value.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/Value.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Java Values} *}
+section {* Java Values *}
 
 theory Value imports Type begin
 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Well-formedness of Java programs} *}
+section {* Well-formedness of Java programs *}
 
 theory WellForm
 imports TypeRel SystemClasses
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Well-typedness Constraints} *}
+section {* Well-typedness Constraints *}
 
 theory WellType imports Term WellForm begin
 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/JVM/JVMDefensive.thy
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Gerwin Klein
 *)
 
-header {* \isaheader{A Defensive JVM} *}
+section {* A Defensive JVM *}
 
 theory JVMDefensive
 imports JVMExec
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/JVM/JVMExceptions.thy
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   2001 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Exception handling in the JVM} *}
+section {* Exception handling in the JVM *}
 
 theory JVMExceptions imports JVMInstructions begin
 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/JVM/JVMExec.thy
--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,7 +3,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Program Execution in the JVM} *}
+section {* Program Execution in the JVM *}
 
 theory JVMExec imports JVMExecInstr JVMExceptions begin
 
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -4,7 +4,7 @@
 *)
 
 
-header {* \isaheader{JVM Instruction Semantics} *}
+section {* JVM Instruction Semantics *}
 
 
 theory JVMExecInstr imports JVMInstructions JVMState begin
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/JVM/JVMInstructions.thy
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Gerwin Klein, Technische Universitaet Muenchen
 *)
 
-header {* \isaheader{Instructions of the JVM} *}
+section {* Instructions of the JVM *}
 
 
 theory JVMInstructions imports JVMState begin
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Stefan Berghofer
 *)
 
-header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *}
+section {* Example for generating executable code from JVM semantics \label{sec:JVMListExample} *}
 
 theory JVMListExample
 imports "../J/SystemClasses" JVMExec
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/JVM/JVMState.thy
--- a/src/HOL/MicroJava/JVM/JVMState.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -2,16 +2,15 @@
     Author:     Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen
 *)
 
-header {* 
-  \chapter{Java Virtual Machine}\label{cha:jvm}
-  \isaheader{State of the JVM} 
-*}
+chapter {* Java Virtual Machine \label{cha:jvm} *}
+
+section {* State of the JVM *}
 
 theory JVMState
 imports "../J/Conform"
 begin
 
-section {* Frame Stack *}
+subsection {* Frame Stack *}
 type_synonym opstack = "val list"
 type_synonym locvars = "val list"
 type_synonym p_count = nat
@@ -30,16 +29,16 @@
   -- "program counter within frame"
 
 
-section {* Exceptions *}
+subsection {* Exceptions *}
 definition raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" where
   "raise_system_xcpt b x \<equiv> raise_if b x None"
 
-section {* Runtime State *}
+subsection {* Runtime State *}
 type_synonym
   jvm_state = "val option \<times> aheap \<times> frame list"  -- "exception flag, heap, frames"
 
 
-section {* Lemmas *}
+subsection {* Lemmas *}
 
 lemma new_Addr_OutOfMemory:
   "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"
diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/document/root.tex
--- a/src/HOL/MicroJava/document/root.tex	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/document/root.tex	Sun Nov 02 17:58:35 2014 +0100
@@ -10,10 +10,7 @@
 \addtolength{\voffset}{-1cm}
 \addtolength{\textheight}{2cm}
 
-\newcommand{\isaheader}[1]
-{\newpage\markright{Theory~\isabellecontext}\section{#1}}
-\renewcommand{\isamarkupheader}[1]{#1}
-\renewcommand{\isamarkupsection}[1]{\subsection{#1}}
+\renewcommand{\setisabellecontext}[1]{\markright{Theory~#1}}
 
 \newcommand{\mJava}{$\mu$Java}
 \newcommand{\secref}[1]{Section~\ref{#1}}