equal
deleted
inserted
replaced
293 |
293 |
294 lemma fresh_unit: |
294 lemma fresh_unit: |
295 shows "a \<sharp> ()" |
295 shows "a \<sharp> ()" |
296 by (simp add: fresh_def supp_unit) |
296 by (simp add: fresh_def supp_unit) |
297 |
297 |
298 |
|
299 section {* additional eqvt lemmas *} |
298 section {* additional eqvt lemmas *} |
300 |
299 |
301 lemmas [eqvt] = |
300 lemmas [eqvt] = |
302 imp_eqvt [folded induct_implies_def] |
301 imp_eqvt [folded induct_implies_def] |
303 |
302 |
304 (* nominal *) |
303 (* nominal *) |
305 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt |
304 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt |
306 |
305 |
307 (* datatypes *) |
306 (* datatypes *) |
308 Pair_eqvt permute_list.simps |
307 Pair_eqvt permute_list.simps |
309 |
308 |
310 (* sets *) |
309 (* sets *) |