changeset 41589 | bbd861837ebc |
parent 16417 | 9bc16273c2d4 |
child 42463 | f270e3e18be5 |
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Sun Jan 16 15:31:22 2011 +0100 +++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Sun Jan 16 15:53:03 2011 +0100 @@ -1,7 +1,5 @@ (* Title: HOL/MicroJava/JVM/JVMInstructions.thy - ID: $Id$ - Author: Gerwin Klein - Copyright 2000 Technische Universitaet Muenchen + Author: Gerwin Klein, Technische Universitaet Muenchen *) header {* \isaheader{Instructions of the JVM} *}