# HG changeset patch
# User urbanc
# Date 1134753778 -3600
# Node ID d2303e8654a2c73a02774b0dda235ee3160d1102
# Parent  bcf13dbaa3396d1b5c6a33e052eff50d56f887ba
added container-lemma fresh_eqvt


(definition: container-lemma contains all instantiations
 of a lemma from the general theory)

diff -r bcf13dbaa339 -r d2303e8654a2 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Fri Dec 16 18:20:59 2005 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Dec 16 18:22:58 2005 +0100
@@ -817,6 +817,8 @@
        val dj_supp           = thm "nominal.dj_supp";
        val fresh_left_ineq   = thm "nominal.pt_fresh_left_ineq";
        val fresh_left        = thm "nominal.pt_fresh_left";
+       val fresh_bij_ineq    = thm "nominal.pt_fresh_bij_ineq";
+       val fresh_bij         = thm "nominal.pt_fresh_bij";
 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
        (* types; this allows for example to use abs_perm (which is a      *)
@@ -908,6 +910,10 @@
 	      let val thms1 = inst_pt_at [fresh_left]
 		  and thms2 = inst_pt_pt_at_cp [fresh_left_ineq]
 	      in [(("fresh_left", thms1 @ thms2),[])] end
+            ||>> PureThy.add_thmss
+	      let val thms1 = inst_pt_at [fresh_bij]
+		  and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
+	      in [(("fresh_eqvt", thms1 @ thms2),[])] end
 	   end;
 
     in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names)