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