src/HOL/MicroJava/BV/JVMType.thy
changeset 42463 f270e3e18be5
parent 42150 b0c0638c4aad
child 47994 d7c0aa802f0d
     1.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -9,14 +9,13 @@
     1.4  imports JType
     1.5  begin
     1.6  
     1.7 -types
     1.8 -  locvars_type = "ty err list"
     1.9 -  opstack_type = "ty list"
    1.10 -  state_type   = "opstack_type \<times> locvars_type"
    1.11 -  state        = "state_type option err"    -- "for Kildall"
    1.12 -  method_type  = "state_type option list"   -- "for BVSpec"
    1.13 -  class_type   = "sig \<Rightarrow> method_type"
    1.14 -  prog_type    = "cname \<Rightarrow> class_type"
    1.15 +type_synonym locvars_type = "ty err list"
    1.16 +type_synonym opstack_type = "ty list"
    1.17 +type_synonym state_type = "opstack_type \<times> locvars_type"
    1.18 +type_synonym state = "state_type option err"    -- "for Kildall"
    1.19 +type_synonym method_type = "state_type option list"   -- "for BVSpec"
    1.20 +type_synonym class_type = "sig \<Rightarrow> method_type"
    1.21 +type_synonym prog_type = "cname \<Rightarrow> class_type"
    1.22  
    1.23  
    1.24  definition stk_esl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty list esl" where