| changeset 2611 | 3d101f2f817c |
| parent 2566 | a59d8e1e3a17 |
| child 2617 | e44551d067e6 |
| 2610:f5c7375ab465 | 2611:3d101f2f817c |
|---|---|
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 |
9 |
10 (* defined as a single nominal datatype *) |
10 (* defined as a single nominal datatype *) |
11 |
|
12 thm finite_set |
|
11 |
13 |
12 nominal_datatype ty = |
14 nominal_datatype ty = |
13 Var "name" |
15 Var "name" |
14 | Fun "ty" "ty" |
16 | Fun "ty" "ty" |
15 and tys = |
17 and tys = |