| changeset 2733 | 5f6fefdbf055 |
| parent 2679 | e003e5e36bae |
| child 2768 | 639979b7fa6e |
| 2732:9abc4a70540c | 2733:5f6fefdbf055 |
|---|---|
1 theory Nominal2 |
1 theory Nominal2 |
2 imports |
2 imports |
3 Nominal2_Base Nominal2_Eqvt Nominal2_Abs |
3 Nominal2_Base Nominal2_Abs |
4 uses ("nominal_dt_rawfuns.ML") |
4 uses ("nominal_dt_rawfuns.ML") |
5 ("nominal_dt_alpha.ML") |
5 ("nominal_dt_alpha.ML") |
6 ("nominal_dt_quot.ML") |
6 ("nominal_dt_quot.ML") |
7 ("nominal_induct.ML") |
7 ("nominal_induct.ML") |
8 ("nominal_inductive.ML") |
8 ("nominal_inductive.ML") |