| changeset 19834 | 2290cc06049b |
| parent 19772 | 45897b49fdd2 |
| child 19856 | 7408a891424e |
| 19833:3a3f591c838d | 19834:2290cc06049b |
|---|---|
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; *} |
|
14 |
11 |
15 section {* Permutations *} |
12 section {* Permutations *} |
16 (*======================*) |
13 (*======================*) |
17 |
14 |
18 types |
15 types |