src/HOL/MicroJava/BV/LBVJVM.thy
changeset 42463 f270e3e18be5
parent 42150 b0c0638c4aad
child 58886 8a6cac7c7247
     1.1 --- a/src/HOL/MicroJava/BV/LBVJVM.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  imports Typing_Framework_JVM
     1.5  begin
     1.6  
     1.7 -types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> JVMType.state list"
     1.8 +type_synonym prog_cert = "cname \<Rightarrow> sig \<Rightarrow> JVMType.state list"
     1.9  
    1.10  definition check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" where
    1.11    "check_cert G mxs mxr n cert \<equiv> check_types G mxs mxr cert \<and> length cert = n+1 \<and>