| changeset 2943 | 09834ba7ce59 |
| parent 2928 | c537d43c09f1 |
| child 2950 | 0911cb7bf696 |
| 2939:dc003667cd17 | 2943:09834ba7ce59 |
|---|---|
1 theory Nominal2 |
1 theory Nominal2 |
2 imports |
2 imports |
3 Nominal2_Base Nominal2_Abs |
3 Nominal2_Base Nominal2_Abs Nominal2_FCB |
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") |