src/HOL/Isar_Examples/Hoare.thy

--- a/src/HOL/Isar_Examples/Hoare.thy	Tue Feb 22 16:47:18 2011 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Tue Feb 22 17:06:14 2011 +0100
@@ -19,9 +19,8 @@
   \cite[\S6]{Winskel:1993}.  See also @{file "~~/src/HOL/Hoare"} and
   \cite{Nipkow:1998:Winskel}. *}
 
-types
-  'a bexp = "'a set"
-  'a assn = "'a set"
+type_synonym 'a bexp = "'a set"
+type_synonym 'a assn = "'a set"
 
 datatype 'a com =
     Basic "'a => 'a"
@@ -32,8 +31,7 @@
 abbreviation Skip  ("SKIP")
   where "SKIP == Basic id"
 
-types
-  'a sem = "'a => 'a => bool"
+type_synonym 'a sem = "'a => 'a => bool"
 
 primrec iter :: "nat => 'a bexp => 'a sem => 'a sem"
 where