src/HOL/Hoare_Parallel/OG_Com.thy
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 58884 be4d203d35b3
--- a/src/HOL/Hoare_Parallel/OG_Com.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Com.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -14,7 +14,7 @@
 datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
 com"} for non-annotated commands. *}
 
-datatype_new 'a ann_com = 
+datatype 'a ann_com = 
      AnnBasic "('a assn)"  "('a \<Rightarrow> 'a)"         
    | AnnSeq "('a ann_com)"  "('a ann_com)"   
    | AnnCond1 "('a assn)"  "('a bexp)"  "('a ann_com)"  "('a ann_com)"