| changeset 51804 | be6e703908f4 |
| parent 51410 | f0865a641e76 |
| child 53355 | 603e6e97c391 |
| 51803:71260347b7e4 | 51804:be6e703908f4 |
|---|---|
13 begin |
13 begin |
14 |
14 |
15 |
15 |
16 section {* Datatype definition *} |
16 section {* Datatype definition *} |
17 |
17 |
18 data 'a trm = |
18 datatype_new 'a trm = |
19 Var 'a | |
19 Var 'a | |
20 App "'a trm" "'a trm" | |
20 App "'a trm" "'a trm" | |
21 Lam 'a "'a trm" | |
21 Lam 'a "'a trm" | |
22 Lt "('a \<times> 'a trm) fset" "'a trm" |
22 Lt "('a \<times> 'a trm) fset" "'a trm" |
23 |
23 |