equal
deleted
inserted
replaced
329 Rsp.thy/prove_alpha_alphabn |
329 Rsp.thy/prove_alpha_alphabn |
330 16) show that alpha implies alpha_bn (by unduction, needed in following step) |
330 16) show that alpha implies alpha_bn (by unduction, needed in following step) |
331 Rsp.thy/prove_const_rsp |
331 Rsp.thy/prove_const_rsp |
332 17) prove respects for all datatype constructors |
332 17) prove respects for all datatype constructors |
333 (unfold eq_iff and alpha_gen; introduce zero permutations; simp) |
333 (unfold eq_iff and alpha_gen; introduce zero permutations; simp) |
334 Lift.thy/quotient_lift_consts_export |
334 Perm.thy/quotient_lift_consts_export |
335 18) define lifted constructors, fv, bn, alpha_bn, permutations |
335 18) define lifted constructors, fv, bn, alpha_bn, permutations |
336 Perm.thy/define_lifted_perms |
336 Perm.thy/define_lifted_perms |
337 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass |
337 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass |
338 Lift.thy/lift_thm |
338 Lift.thy/lift_thm |
339 20) lift permutation simplifications |
339 20) lift permutation simplifications |