| changeset 12911 | 704713ca07ea |
| parent 12773 | a47f51daa6dc |
| child 13006 | 51c5f3f11d16 |
--- a/src/HOL/MicroJava/BV/Semilat.thy Wed Feb 20 17:30:46 2002 +0100 +++ b/src/HOL/MicroJava/BV/Semilat.thy Thu Feb 21 09:54:08 2002 +0100 @@ -6,7 +6,10 @@ Semilattices *) -header "Semilattices" +header {* + \chapter{Bytecode Verifier}\label{cha:bv} + \isaheader{Semilattices} +*} theory Semilat = While_Combinator: