changeset 12911 | 704713ca07ea |
parent 12516 | d09d0f160888 |
child 12978 | 16cc829b9c65 |
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Wed Feb 20 17:30:46 2002 +0100 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy Thu Feb 21 09:54:08 2002 +0100 @@ -4,7 +4,7 @@ Copyright 1999 Technische Universitaet Muenchen *) -header {* The Lightweight Bytecode Verifier *} +header {* \isaheader{The Lightweight Bytecode Verifier} *} theory LBVSpec = Effect + Kildall: