added generalised definitions for freshness of sets of atoms
and lists of atoms

--- a/src/HOL/Nominal/Nominal.thy	Wed Apr 02 15:58:57 2008 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Thu Apr 03 11:48:48 2008 +0200
@@ -393,6 +393,19 @@
   Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
 *}
 
+section {* generalisation of freshness to lists and sets of atoms *}
+(*================================================================*)
+ 
+consts
+  fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
+
+defs (overloaded)
+  fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x\<in>xs. x\<sharp>c"
+
+defs (overloaded)
+  fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x\<in>set xs. x\<sharp>c"
+
+lemmas fresh_star_def = fresh_star_list fresh_star_set
 
 section {* Abstract Properties for Permutations and  Atoms *}
 (*=========================================================*)