| changeset 11237 | 0ef5ecc1fd4d |
| parent 11236 | 17403c5a9eb1 |
| child 11292 | d838df879585 |
| 11236:17403c5a9eb1 | 11237:0ef5ecc1fd4d |
|---|---|
291 datatype lambda = C "lambda \<Rightarrow> lambda" |
291 datatype lambda = C "lambda \<Rightarrow> lambda" |
292 *) |
292 *) |
293 |
293 |
294 text{* |
294 text{* |
295 \begin{exercise} |
295 \begin{exercise} |
296 Define a datatype of ordinals and the ordinal Gamma0. |
296 Define a datatype of ordinals and the ordinal $\Gamma_0$. |
297 \end{exercise} |
297 \end{exercise} |
298 *} |
298 *} |
299 |
299 |
300 end |
300 end |