equal
deleted
inserted
replaced
22 |
22 |
23 |
23 |
24 section {* eqvt lemmas *} |
24 section {* eqvt lemmas *} |
25 |
25 |
26 lemmas [eqvt] = |
26 lemmas [eqvt] = |
27 conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt uminus_eqvt |
27 conj_eqvt Not_eqvt ex_eqvt all_eqvt ex1_eqvt imp_eqvt uminus_eqvt |
28 imp_eqvt[folded induct_implies_def] |
28 imp_eqvt[folded induct_implies_def] |
29 all_eqvt[folded induct_forall_def] |
29 all_eqvt[folded induct_forall_def] |
30 |
30 |
31 (* nominal *) |
31 (* nominal *) |
32 supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt |
32 supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt |