src/HOL/MicroJava/JVM/JVMState.thy
changeset 42463 f270e3e18be5
parent 41589 bbd861837ebc
child 58886 8a6cac7c7247
     1.1 --- a/src/HOL/MicroJava/JVM/JVMState.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMState.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -12,11 +12,11 @@
     1.4  begin
     1.5  
     1.6  section {* Frame Stack *}
     1.7 -types
     1.8 - opstack   = "val list"
     1.9 - locvars   = "val list" 
    1.10 - p_count   = nat
    1.11 +type_synonym opstack = "val list"
    1.12 +type_synonym locvars = "val list"
    1.13 +type_synonym p_count = nat
    1.14  
    1.15 +type_synonym
    1.16   frame = "opstack \<times>     
    1.17            locvars \<times>   
    1.18            cname \<times>     
    1.19 @@ -35,7 +35,7 @@
    1.20    "raise_system_xcpt b x \<equiv> raise_if b x None"
    1.21  
    1.22  section {* Runtime State *}
    1.23 -types
    1.24 +type_synonym
    1.25    jvm_state = "val option \<times> aheap \<times> frame list"  -- "exception flag, heap, frames"
    1.26  
    1.27