--- a/src/HOL/MicroJava/BV/BVSpec.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Thu Feb 21 09:54:08 2002 +0100
@@ -5,7 +5,7 @@
*)
-header "The Bytecode Verifier"
+header {* \isaheader{The Bytecode Verifier}\label{sec:BVSpec} *}
theory BVSpec = Effect: