# HG changeset patch
# User narboux
# Date 1177529354 -7200
# Node ID d0f483fd57ddad7da08f2d9fffb7a61469e43115
# Parent  dc13dfd588b243921d124ec8fec331df1d28dcca
add the lemma supp_eqvt and put the right attribute

diff -r dc13dfd588b2 -r d0f483fd57dd src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Wed Apr 25 17:50:48 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Apr 25 21:29:14 2007 +0200
@@ -717,6 +717,8 @@
        val fresh_perm_app_ineq = thm "Nominal.pt_fresh_perm_app_ineq";
        val fresh_perm_app      = thm "Nominal.pt_fresh_perm_app";	
        val fresh_aux           = thm "Nominal.pt_fresh_aux";  
+       val pt_perm_supp_ineq   = thm "Nominal.pt_perm_supp_ineq";
+       val pt_perm_supp        = thm "Nominal.pt_perm_supp";
 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
        (* types; this allows for example to use abs_perm (which is a      *)
@@ -862,7 +864,11 @@
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [fresh_perm_app]
 		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
-	      in  [(("fresh_perm_app", thms1 @ thms2),[])] end  
+	      in  [(("fresh_perm_app", thms1 @ thms2),[])] end 
+            ||>> PureThy.add_thmss
+	      let val thms1 = inst_pt_at [pt_perm_supp]
+		  and thms2 = inst_pt_pt_at_cp [pt_perm_supp_ineq] 
+	      in  [(("supp_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end  
             ||>> PureThy.add_thmss [(("fin_supp",fs_axs),[])]
 	   end;