equal
deleted
inserted
replaced
3 |
3 |
4 Equivariance, Supp and Fresh Lemmas for Operators. |
4 Equivariance, Supp and Fresh Lemmas for Operators. |
5 (Contains most, but not all such lemmas.) |
5 (Contains most, but not all such lemmas.) |
6 *) |
6 *) |
7 theory Nominal2_Eqvt |
7 theory Nominal2_Eqvt |
8 imports Nominal2_Base |
8 imports Nominal2_Base Nominal2_Atoms |
9 uses ("nominal_thmdecls.ML") |
9 uses ("nominal_thmdecls.ML") |
10 ("nominal_permeq.ML") |
10 ("nominal_permeq.ML") |
11 begin |
11 begin |
12 |
12 |
13 section {* Logical Operators *} |
13 section {* Logical Operators *} |
246 permute_prod.simps append_eqvt rev_eqvt set_eqvt |
246 permute_prod.simps append_eqvt rev_eqvt set_eqvt |
247 fst_eqvt snd_eqvt |
247 fst_eqvt snd_eqvt |
248 |
248 |
249 (* sets *) |
249 (* sets *) |
250 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt |
250 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt |
251 Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt |
251 Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt |
|
252 |
|
253 atom_eqvt |
252 |
254 |
253 thm eqvts |
255 thm eqvts |
254 thm eqvts_raw |
256 thm eqvts_raw |
255 |
257 |
256 text {* helper lemmas for the eqvt_tac *} |
258 text {* helper lemmas for the eqvt_tac *} |