diff -r 9a8decba77c5 -r b435ee87d9c8 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 14 16:10:44 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 14 16:11:04 2010 +0200
@@ -9,6 +9,7 @@
 imports Nominal2_Base Nominal2_Atoms
 uses ("nominal_thmdecls.ML")
      ("nominal_permeq.ML")
+     ("nominal_eqvt.ML")
 begin
 
 
@@ -284,6 +285,7 @@
   shows "p \<bullet> unpermute p x \<equiv> x"
   unfolding unpermute_def by simp
 
+(* provides perm_simp methods *)
 use "nominal_permeq.ML"
 setup Nominal_Permeq.setup
 
@@ -371,4 +373,8 @@
 (* apply(perm_strict_simp) *)
 oops
 
+(* automatic equivariance procedure for 
+   inductive definitions *)
+use "nominal_eqvt.ML"
+
 end