src/HOL/MicroJava/JVM/JVMInstructions.thy
changeset 42463 f270e3e18be5
parent 41589 bbd861837ebc
child 58249 180f1b3508ed
     1.1 --- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -28,13 +28,17 @@
     1.4          | Ifcmpeq int               -- "branch if int/ref comparison succeeds"
     1.5          | Throw                     -- "throw top of stack as exception"
     1.6  
     1.7 -types
     1.8 +type_synonym
     1.9    bytecode = "instr list"
    1.10 +type_synonym
    1.11    exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" 
    1.12                    -- "start-pc, end-pc, handler-pc, exception type"
    1.13 +type_synonym
    1.14    exception_table = "exception_entry list"
    1.15 +type_synonym
    1.16    jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table"
    1.17     -- "max stacksize, size of register set, instruction sequence, handler table"
    1.18 +type_synonym
    1.19    jvm_prog = "jvm_method prog" 
    1.20  
    1.21  end