| changeset 1774 | c34347ec7ab3 |
| parent 1682 | ae54ce4cde54 |
| child 1782 | 27fec5fcfe67 |
| 1773:c0eac04ae3b4 | 1774:c34347ec7ab3 |
|---|---|
1 theory Nominal2_FSet |
1 theory Nominal2_FSet |
2 imports FSet Nominal2_Supp |
2 imports FSet "../Nominal-General/Nominal2_Supp" |
3 begin |
3 begin |
4 |
4 |
5 lemma permute_rsp_fset[quot_respect]: |
5 lemma permute_rsp_fset[quot_respect]: |
6 "(op = ===> list_eq ===> list_eq) permute permute" |
6 "(op = ===> list_eq ===> list_eq) permute permute" |
7 apply (simp add: eqvts[symmetric]) |
7 apply (simp add: eqvts[symmetric]) |