# HG changeset patch
# User urbanc
# Date 1146615383 -7200
# Node ID c0a89682819411cb1336b73c036afeeaeb6b0def
# Parent  17f504343d0f63416dd48340c5c978d5caf3fcc7
added lemma fresh_right, which is useful
in the proof of the recursion combinator

diff -r 17f504343d0f -r c0a896828194 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue May 02 20:42:43 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Wed May 03 02:16:23 2006 +0200
@@ -672,6 +672,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_right_ineq    = thm "Nominal.pt_fresh_right_ineq";
+       val fresh_right         = thm "Nominal.pt_fresh_right";
        val fresh_bij_ineq      = thm "Nominal.pt_fresh_bij_ineq";
        val fresh_bij           = thm "Nominal.pt_fresh_bij";
        val pt_pi_rev           = thm "Nominal.pt_pi_rev";
@@ -780,6 +782,10 @@
 		  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_right]
+		  and thms2 = inst_pt_pt_at_cp [fresh_right_ineq]
+	      in [(("fresh_right", 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