src/HOL/Hoare/Hoare_Logic.thy
changeset 58310 91ea607a34d8
parent 58305 57752a91eec4
child 62042 6c6ccf573479
--- a/src/HOL/Hoare/Hoare_Logic.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -15,7 +15,7 @@
 type_synonym 'a bexp = "'a set"
 type_synonym 'a assn = "'a set"
 
-datatype_new 'a com =
+datatype 'a com =
   Basic "'a \<Rightarrow> 'a"
 | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
 | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)