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