diff -r c748d11547d8 -r 2ebad1cb045f src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Oct 24 12:08:33 2002 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Oct 25 10:47:47 2002 +0200
@@ -38,7 +38,7 @@
 
 
 (********************************************************************************)
-(**** Stuff about index ****)
+section "index"
 
 lemma local_env_snd: "
   snd (local_env G C (mn, pTs) pns lvars) = map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)"
@@ -201,7 +201,7 @@
 
 (********************************************************************************)
 
-(* Preservation of ST and LT by compTpExpr / compTpStmt *)
+section "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)
@@ -816,7 +816,7 @@
 
 
   (* ********************************************************************** *)
-  (* length of compExpr/ compTpExprs *)
+section "length of compExpr/ compTpExprs"
   (* ********************************************************************** *)
 
 lemma length_comb [simp]:  "length (mt_of ((f1 \<box> f2) sttp)) = 
@@ -882,7 +882,7 @@
 
 
   (* ********************************************************************** *)
-  (* Correspondence bytecode - method types *)
+section "Correspondence bytecode - method types"
   (* ********************************************************************** *)
 
 syntax
@@ -2613,7 +2613,7 @@
 apply auto
 done
 
-
+section "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)"