# HG changeset patch
# User urbanc
# Date 1175346832 -7200
# Node ID 6775c71f1da0226114d2638efda5a5934618c8ab
# Parent  b067fdca022dfcbb6efdf7389d7a9993515183ce
added pt_bij' to the collection perm_swap and also added abs_perm to the collection of equivariance lemmas

diff -r b067fdca022d -r 6775c71f1da0 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 31 12:40:55 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 31 15:13:52 2007 +0200
@@ -685,6 +685,7 @@
        val abs_fun_supp        = thm "Nominal.abs_fun_supp";
        val abs_fun_supp_ineq   = thm "Nominal.abs_fun_supp_ineq";
        val pt_swap_bij         = thm "Nominal.pt_swap_bij";
+       val pt_swap_bij'        = thm "Nominal.pt_swap_bij'";
        val pt_fresh_fresh      = thm "Nominal.pt_fresh_fresh";
        val pt_bij              = thm "Nominal.pt_bij";
        val pt_perm_compose     = thm "Nominal.pt_perm_compose";
@@ -783,7 +784,7 @@
             thy32 
 	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
             ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])]
-            ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])]
+            ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])]
             ||>> PureThy.add_thmss 
 	      let val thms1 = inst_pt_at [pt_pi_rev];
 		  val thms2 = inst_pt_at [pt_rev_pi];
@@ -813,7 +814,7 @@
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [abs_fun_pi]
 		  and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]
-	      in [(("abs_perm", thms1 @ thms2),[])] end
+	      in [(("abs_perm", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_dj [dj_perm_forget]
 		  and thms2 = inst_dj [dj_pp_forget]