| changeset 12911 | 704713ca07ea |
| parent 12774 | 501da8288f05 |
| child 13006 | 51c5f3f11d16 |
--- a/src/HOL/MicroJava/BV/Correct.thy Wed Feb 20 17:30:46 2002 +0100 +++ b/src/HOL/MicroJava/BV/Correct.thy Thu Feb 21 09:54:08 2002 +0100 @@ -7,7 +7,7 @@ The invariant for the type safety proof. *) -header "BV Type Safety Invariant" +header {* \isaheader{BV Type Safety Invariant} *} theory Correct = BVSpec + JVMExec: