diff -r deb732753522 -r ace7775cbd04 Nominal/Ex/ExLetRec.thy --- a/Nominal/Ex/ExLetRec.thy Wed May 05 20:39:56 2010 +0100 +++ b/Nominal/Ex/ExLetRec.thy Thu May 06 10:43:41 2010 +0200 @@ -75,6 +75,12 @@ apply (simp add: atom_eqvt fresh_star_def) done +(* +declare permute_trm_raw_permute_lts_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] +equivariance alpha_trm_raw +*) + end