src/HOL/Hoare_Parallel/OG_Com.thy
changeset 42174 d0be2722ce9f
parent 39246 9e58f0499f57
child 58249 180f1b3508ed
--- a/src/HOL/Hoare_Parallel/OG_Com.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Com.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -7,9 +7,8 @@
 
 text {* Type abbreviations for boolean expressions and assertions: *}
 
-types
-    'a bexp = "'a set"
-    'a assn = "'a set"
+type_synonym 'a bexp = "'a set"
+type_synonym 'a assn = "'a set"
 
 text {* The syntax of commands is defined by two mutually recursive
 datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a