--- a/src/HOL/MicroJava/J/Conform.thy Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Sat Apr 23 13:00:19 2011 +0200
@@ -7,7 +7,7 @@
theory Conform imports State WellType Exceptions begin
-types 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}"
+type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}"
definition hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) where
"h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"