changeset 10591 | 6d6cb845e841 |
parent 10057 | 8c8d2d0d3ef8 |
child 10897 | 697fab84709e |
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Tue Dec 05 08:22:49 2000 +0100 +++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Tue Dec 05 14:08:22 2000 +0100 @@ -33,6 +33,6 @@ types bytecode = "instr list" - jvm_prog = "(nat \<times> bytecode) prog" + jvm_prog = "(nat \<times> nat \<times> bytecode) prog" end