| changeset 2635 | 64b4cb2c2bf8 |
| parent 2616 | dd7490fdd998 |
| child 2659 | 619ecb57db38 |
| 2634:3ce1089cdbf3 | 2635:64b4cb2c2bf8 |
|---|---|
1 theory Nominal2_Abs |
1 theory Nominal2_Abs |
2 imports "Nominal2_Base" |
2 imports "Nominal2_Base" |
3 "Nominal2_Eqvt" |
3 "Nominal2_Eqvt" |
4 "Quotient" |
4 "~~/src/HOL/Quotient" |
5 "Quotient_List" |
5 "~~/src/HOL/Library/Quotient_List" |
6 "Quotient_Product" |
6 "~~/src/HOL/Library/Quotient_Product" |
7 begin |
7 begin |
8 |
8 |
9 |
9 |
10 section {* Abstractions *} |
10 section {* Abstractions *} |
11 |
11 |