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