diff -r 92195e8c6208 -r da7345ff18e1 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Wed Feb 27 21:53:54 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Thu Feb 28 13:38:49 2002 +0100
@@ -3,10 +3,18 @@
     Author:     Gerwin Klein
 *)
 
-header {* Example Welltypings *}
+header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
 
 theory BVExample = JVMListExample + Correct:
 
+text {*
+  This theory shows type correctness of the example program in section 
+  \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by
+  explicitly providing a welltyping. It also shows that the start
+  state of the program conforms to the welltyping; hence type safe
+  execution is guaranteed.
+*}
+
 section "Setup"
 text {*
   Since the types @{typ cnam}, @{text vnam}, and @{text mname} are