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