changeset 2471 | 894599a50af3 |
parent 2468 | 7b1470b55936 |
child 2524 | 693562f03eee |
2470:bdb1eab47161 | 2471:894599a50af3 |
---|---|
1 theory Nominal2_FSet |
1 theory Nominal2_FSet |
2 imports "../Nominal-General/Nominal2_Base" |
2 imports "../Nominal-General/Nominal2_Base" |
3 "../Nominal-General/Nominal2_Supp" |
|
4 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
5 FSet |
4 FSet |
6 begin |
5 begin |
7 |
6 |
8 lemma permute_rsp_fset[quot_respect]: |
7 lemma permute_rsp_fset[quot_respect]: |