| changeset 1806 | 90095f23fc60 |
| parent 1782 | 27fec5fcfe67 |
| child 1815 | 4135198bbb8a |
| 1805:f187f20f0a79 | 1806:90095f23fc60 |
|---|---|
1 theory Nominal2_FSet |
1 theory Nominal2_FSet |
2 imports FSet "../Nominal-General/Nominal2_Supp" |
2 imports "../Nominal-General/Nominal2_Supp" |
3 FSet |
|
3 begin |
4 begin |
4 |
5 |
5 lemma permute_rsp_fset[quot_respect]: |
6 lemma permute_rsp_fset[quot_respect]: |
6 "(op = ===> list_eq ===> list_eq) permute permute" |
7 "(op = ===> list_eq ===> list_eq) permute permute" |
7 apply (simp add: eqvts[symmetric]) |
8 apply (simp add: eqvts[symmetric]) |