
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
 
 




