| changeset 58310 | 91ea607a34d8 |
| parent 58309 | a09ec6daaa19 |
| child 58889 | 5b7a9633cfa8 |
| 58309:a09ec6daaa19 | 58310:91ea607a34d8 |
|---|---|
12 imports "~~/src/HOL/Library/FSet" |
12 imports "~~/src/HOL/Library/FSet" |
13 begin |
13 begin |
14 |
14 |
15 section {* Datatype definition *} |
15 section {* Datatype definition *} |
16 |
16 |
17 datatype_new 'a trm = |
17 datatype 'a trm = |
18 Var 'a | |
18 Var 'a | |
19 App "'a trm" "'a trm" | |
19 App "'a trm" "'a trm" | |
20 Lam 'a "'a trm" | |
20 Lam 'a "'a trm" | |
21 Lt "('a \<times> 'a trm) fset" "'a trm" |
21 Lt "('a \<times> 'a trm) fset" "'a trm" |
22 |
22 |