src/HOL/MicroJava/J/Conform.thy
changeset 42463 f270e3e18be5
parent 37139 e0bd5934a2fb
child 42793 88bee9f6eec7
     1.1 --- a/src/HOL/MicroJava/J/Conform.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  theory Conform imports State WellType Exceptions begin
     1.6  
     1.7 -types 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"
     1.8 +type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"
     1.9  
    1.10  definition hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) where
    1.11   "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"