src/HOL/MicroJava/JVM/JVMInstructions.thy
changeset 58249 180f1b3508ed
parent 42463 f270e3e18be5
child 58310 91ea607a34d8
equal deleted inserted replaced
58248:25af24e1f37b 58249:180f1b3508ed
     6 
     6 
     7 
     7 
     8 theory JVMInstructions imports JVMState begin
     8 theory JVMInstructions imports JVMState begin
     9 
     9 
    10 
    10 
    11 datatype 
    11 datatype_new 
    12   instr = Load nat                  -- "load from local variable"
    12   instr = Load nat                  -- "load from local variable"
    13         | Store nat                 -- "store into local variable"
    13         | Store nat                 -- "store into local variable"
    14         | LitPush val               -- "push a literal (constant)"
    14         | LitPush val               -- "push a literal (constant)"
    15         | New cname                 -- "create object"
    15         | New cname                 -- "create object"
    16         | Getfield vname cname      -- "Fetch field from object"
    16         | Getfield vname cname      -- "Fetch field from object"