# HG changeset patch
# User berghofe
# Date 1201170191 -3600
# Node ID a3067f6f08a2548f67afe09f58e4ba6859ec3d31
# Parent  850b4c2d0f178764a2aadda76e5fb67a5a42ccf7
Added lemma at_fin_set_fresh.

diff -r 850b4c2d0f17 -r a3067f6f08a2 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Jan 23 23:35:23 2008 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Thu Jan 24 11:23:11 2008 +0100
@@ -1947,6 +1947,13 @@
   then show "X\<subseteq>(supp X)" by blast
 qed
 
+lemma at_fin_set_fresh:
+  fixes X::"'x set" 
+  assumes at: "at TYPE('x)"
+  and     fs: "finite X"
+  shows "(x \<sharp> X) = (x \<notin> X)"
+  by (simp add: at_fin_set_supp fresh_def at fs)
+
 section {* Permutations acting on Functions *}
 (*==========================================*)