src/HOL/Hoare_Parallel/RG_Com.thy
changeset 42174 d0be2722ce9f
parent 32621 a073cb249a06
child 58249 180f1b3508ed
     1.1 --- a/src/HOL/Hoare_Parallel/RG_Com.thy	Wed Mar 30 22:53:18 2011 +0200
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Com.thy	Wed Mar 30 23:26:40 2011 +0200
     1.3 @@ -10,8 +10,7 @@
     1.4  of states.  Syntax of commands @{text com} and parallel commands
     1.5  @{text par_com}. *}
     1.6  
     1.7 -types
     1.8 -  'a bexp = "'a set"
     1.9 +type_synonym 'a bexp = "'a set"
    1.10  
    1.11  datatype 'a com = 
    1.12      Basic "'a \<Rightarrow>'a"
    1.13 @@ -20,6 +19,6 @@
    1.14    | While "'a bexp" "'a com"       
    1.15    | Await "'a bexp" "'a com"                 
    1.16  
    1.17 -types 'a par_com = "(('a com) option) list"
    1.18 +type_synonym 'a par_com = "'a com option list"
    1.19  
    1.20  end
    1.21 \ No newline at end of file