changeset 12911 | 704713ca07ea |
parent 12772 | 7b7051ae49a0 |
child 12951 | a9fdcb71d252 |
--- a/src/HOL/MicroJava/BV/Effect.thy Wed Feb 20 17:30:46 2002 +0100 +++ b/src/HOL/MicroJava/BV/Effect.thy Thu Feb 21 09:54:08 2002 +0100 @@ -4,7 +4,7 @@ Copyright 2000 Technische Universitaet Muenchen *) -header {* Effect of Instructions on the State Type *} +header {* \isaheader{Effect of Instructions on the State Type} *} theory Effect = JVMType + JVMExceptions: