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)"