equal
deleted
inserted
replaced
237 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
237 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
238 True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt |
238 True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt |
239 imp_eqvt [folded induct_implies_def] |
239 imp_eqvt [folded induct_implies_def] |
240 |
240 |
241 (* nominal *) |
241 (* nominal *) |
242 permute_eqvt supp_eqvt fresh_eqvt |
242 (*permute_eqvt commented out since it loops *) |
|
243 supp_eqvt fresh_eqvt |
243 permute_pure |
244 permute_pure |
244 |
245 |
245 (* datatypes *) |
246 (* datatypes *) |
246 permute_prod.simps append_eqvt rev_eqvt set_eqvt |
247 permute_prod.simps append_eqvt rev_eqvt set_eqvt |
247 fst_eqvt snd_eqvt |
248 fst_eqvt snd_eqvt |