equal
deleted
inserted
replaced
24 section {* eqvt lemmas *} |
24 section {* eqvt lemmas *} |
25 |
25 |
26 lemmas [eqvt] = |
26 lemmas [eqvt] = |
27 conj_eqvt Not_eqvt ex_eqvt imp_eqvt |
27 conj_eqvt Not_eqvt ex_eqvt imp_eqvt |
28 imp_eqvt[folded induct_implies_def] |
28 imp_eqvt[folded induct_implies_def] |
|
29 uminus_eqvt |
29 |
30 |
30 (* nominal *) |
31 (* nominal *) |
31 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt |
32 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt |
|
33 swap_eqvt flip_eqvt |
32 |
34 |
33 (* datatypes *) |
35 (* datatypes *) |
34 Pair_eqvt permute_list.simps |
36 Pair_eqvt permute_list.simps |
35 |
37 |
36 |
38 |