equal
deleted
inserted
replaced
249 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
249 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
250 True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt |
250 True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt |
251 imp_eqvt [folded induct_implies_def] |
251 imp_eqvt [folded induct_implies_def] |
252 |
252 |
253 (* nominal *) |
253 (* nominal *) |
254 supp_eqvt fresh_eqvt add_perm_eqvt |
254 supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt |
255 |
255 |
256 (* datatypes *) |
256 (* datatypes *) |
257 permute_prod.simps append_eqvt rev_eqvt set_eqvt |
257 permute_prod.simps append_eqvt rev_eqvt set_eqvt |
258 map_eqvt fst_eqvt snd_eqvt Pair_eqvt permute_list.simps |
258 map_eqvt fst_eqvt snd_eqvt Pair_eqvt permute_list.simps |
259 |
259 |