| changeset 19751 | 3006498da5c5 |
| parent 19687 | 0a7c6d78ad6b |
| child 19771 | b4a0da62126e |
| 19750:5281bd607206 | 19751:3006498da5c5 |
|---|---|
6 ("nominal_atoms.ML") |
6 ("nominal_atoms.ML") |
7 ("nominal_package.ML") |
7 ("nominal_package.ML") |
8 ("nominal_induct.ML") |
8 ("nominal_induct.ML") |
9 ("nominal_permeq.ML") |
9 ("nominal_permeq.ML") |
10 begin |
10 begin |
11 |
|
12 (* FIXME: this needs to be corrected in nominal_package *) |
|
13 ML {* reset NameSpace.unique_names; *} |
|
11 |
14 |
12 section {* Permutations *} |
15 section {* Permutations *} |
13 (*======================*) |
16 (*======================*) |
14 |
17 |
15 types |
18 types |