equal
deleted
inserted
replaced
1 theory Nominal2_FSet |
1 theory Nominal2_FSet |
2 imports "../Nominal-General/Nominal2_Base" |
2 imports "../Nominal-General/Nominal2_Base" |
3 "../Nominal-General/Nominal2_Eqvt" |
3 "../Nominal-General/Nominal2_Eqvt" |
4 FSet |
4 "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet" |
5 begin |
5 begin |
6 |
6 |
7 lemma permute_fset_rsp[quot_respect]: |
7 lemma permute_fset_rsp[quot_respect]: |
8 shows "(op = ===> list_eq ===> list_eq) permute permute" |
8 shows "(op = ===> list_eq ===> list_eq) permute permute" |
9 by (simp add: set_eqvt[symmetric]) |
9 by (simp add: set_eqvt[symmetric]) |