changeset 58249 | 180f1b3508ed |
parent 42463 | f270e3e18be5 |
child 58310 | 91ea607a34d8 |
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Tue Sep 09 20:51:36 2014 +0200 @@ -8,7 +8,7 @@ theory JVMInstructions imports JVMState begin -datatype +datatype_new instr = Load nat -- "load from local variable" | Store nat -- "store into local variable" | LitPush val -- "push a literal (constant)"