equal
deleted
inserted
replaced
19 \cite{Nipkow:1998:Winskel}. *} |
19 \cite{Nipkow:1998:Winskel}. *} |
20 |
20 |
21 type_synonym 'a bexp = "'a set" |
21 type_synonym 'a bexp = "'a set" |
22 type_synonym 'a assn = "'a set" |
22 type_synonym 'a assn = "'a set" |
23 |
23 |
24 datatype_new 'a com = |
24 datatype 'a com = |
25 Basic "'a \<Rightarrow> 'a" |
25 Basic "'a \<Rightarrow> 'a" |
26 | Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60) |
26 | Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60) |
27 | Cond "'a bexp" "'a com" "'a com" |
27 | Cond "'a bexp" "'a com" "'a com" |
28 | While "'a bexp" "'a assn" "'a com" |
28 | While "'a bexp" "'a assn" "'a com" |
29 |
29 |