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)