equal
deleted
inserted
replaced
60 *} |
60 *} |
61 |
61 |
62 |
62 |
63 section {* NOT *} |
63 section {* NOT *} |
64 |
64 |
65 lemma [quot_respect]: |
|
66 "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw" |
|
67 sorry |
|
68 |
|
69 |
|
70 ML {* |
65 ML {* |
71 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) |
66 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) |
72 @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
67 @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
73 prod.cases]} |
68 prod.cases]} |
74 *} |
69 *} |