| changeset 2129 | f38adea0591c |
| parent 2080 | 0532006ec7ec |
| child 2200 | 31f1ec832d39 |
| 2128:abd46dfc0212 | 2129:f38adea0591c |
|---|---|
300 |
300 |
301 lemmas [eqvt] = |
301 lemmas [eqvt] = |
302 imp_eqvt [folded induct_implies_def] |
302 imp_eqvt [folded induct_implies_def] |
303 |
303 |
304 (* nominal *) |
304 (* nominal *) |
305 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt |
305 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt |
306 |
306 |
307 (* datatypes *) |
307 (* datatypes *) |
308 Pair_eqvt permute_list.simps |
308 Pair_eqvt permute_list.simps |
309 |
309 |
310 (* sets *) |
310 (* sets *) |