changeset 2105 | e25b0fff0dd2 |
parent 2104 | 2205b572bc9b |
child 2120 | 2786ff1df475 |
--- a/Nominal/Ex/ExLet.thy Tue May 11 17:16:57 2010 +0200 +++ b/Nominal/Ex/ExLet.thy Tue May 11 18:20:25 2010 +0200 @@ -34,12 +34,7 @@ (*thm trm_lts.supp*) thm trm_lts.fv[simplified trm_lts.supp(1-2)] - -declare permute_trm_raw_permute_lts_raw.simps[eqvt] - -equivariance alpha_trm_raw - - +equivariance alpha_bn_raw primrec permute_bn_raw