| changeset 2733 | 5f6fefdbf055 |
| parent 2730 | eebc24b9cf39 |
| child 2843 | 1ae3c9b2d557 |
| 2732:9abc4a70540c | 2733:5f6fefdbf055 |
|---|---|
1 theory Nominal2_Abs |
1 theory Nominal2_Abs |
2 imports "Nominal2_Base" |
2 imports "Nominal2_Base" |
3 "Nominal2_Eqvt" |
|
4 "~~/src/HOL/Quotient" |
3 "~~/src/HOL/Quotient" |
5 "~~/src/HOL/Library/Quotient_List" |
4 "~~/src/HOL/Library/Quotient_List" |
6 "~~/src/HOL/Library/Quotient_Product" |
5 "~~/src/HOL/Library/Quotient_Product" |
7 begin |
6 begin |
8 |
7 |