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