src/HOL/Hoare_Parallel/RG_Com.thy

 of states.  Syntax of commands @{text com} and parallel commands
 @{text par_com}. *}
 
 type_synonym 'a bexp = "'a set"
 
-datatype_new 'a com = 
+datatype 'a com = 
     Basic "'a \<Rightarrow>'a"
   | Seq "'a com" "'a com"
   | Cond "'a bexp" "'a com" "'a com"         
   | While "'a bexp" "'a com"       
   | Await "'a bexp" "'a com"