Nominal/Ex/ExLetRec.thy
changeset 2067 ace7775cbd04
parent 2041 3842464ee03b
child 2082 0854af516f14
--- 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