| changeset 2314 | 1a14c4171a51 |
| parent 2313 | 25d2cdf7d7e4 |
| child 2316 | 08bbde090a17 |
| 2313:25d2cdf7d7e4 | 2314:1a14c4171a51 |
|---|---|
3 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
4 "../Nominal-General/Nominal2_Supp" |
4 "../Nominal-General/Nominal2_Supp" |
5 "Perm" "Tacs" "Equivp" "Lift" |
5 "Perm" "Tacs" "Equivp" "Lift" |
6 begin |
6 begin |
7 |
7 |
8 (* TODO |
|
9 |
|
10 we need to also export a cases-rule for nominal datatypes |
|
11 size function |
|
12 *) |
|
8 |
13 |
9 section{* Interface for nominal_datatype *} |
14 section{* Interface for nominal_datatype *} |
10 |
15 |
11 |
16 |
12 ML {* |
17 ML {* |