--- a/Nominal-General/Nominal2_Eqvt.thy	Mon Apr 26 08:19:11 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Mon Apr 26 13:08:14 2010 +0200
@@ -235,6 +235,7 @@
 apply(simp)
 done
 
+
 section {* Equivariance automation *}
 
 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
@@ -242,6 +243,7 @@
 use "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"
 
+ML {* Thm.full_rules *}
 lemmas [eqvt] = 
   (* connectives *)
   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 
@@ -369,6 +371,15 @@
 apply(perm_simp exclude: The)
 oops
 
+
+thm eqvts
+thm eqvts_raw
+
+ML {*
+Nominal_ThmDecls.is_eqvt @{context} @{term "supp"}
+*}
+
+
 (* automatic equivariance procedure for 
    inductive definitions *)
 use "nominal_eqvt.ML"