changeset 2467 | 67b3933c3190 |
parent 2466 | 47c840599a6b |
child 2468 | 7b1470b55936 |
2466:47c840599a6b | 2467:67b3933c3190 |
---|---|
1 theory Nominal2_FSet |
1 theory Nominal2_FSet |
2 imports "../Nominal-General/Nominal2_Supp" |
2 imports "../Nominal-General/Nominal2_Base" |
3 "../Nominal-General/Nominal2_Atoms" |
3 "../Nominal-General/Nominal2_Supp" |
4 "../Nominal-General/Nominal2_Eqvt" |
4 "../Nominal-General/Nominal2_Eqvt" |
5 FSet |
5 FSet |
6 begin |
6 begin |
7 |
7 |
8 lemma permute_rsp_fset[quot_respect]: |
8 lemma permute_rsp_fset[quot_respect]: |