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