--- 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)"