src/HOL/MicroJava/BV/LBVComplete.thy

--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Jun 07 17:14:04 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Jun 07 17:14:19 2000 +0200
@@ -2,9 +2,9 @@
     ID:         $Id$
     Author:     Gerwin Klein
     Copyright   2000 Technische Universitaet Muenchen
+*)
 
-Proof of completeness for the lightweight bytecode verifier
-*)
+header {* Completeness of the LBV *}
 
 theory LBVComplete = LBVSpec:;