# HG changeset patch
# User urbanc
# Date 1207216128 -7200
# Node ID b05cdd060c3e569a7c7e84d1c825aa273e23a513
# Parent  f8c4e79db153a0a48eb53af98412ca589962ad63
added generalised definitions for freshness of sets of atoms
and lists of atoms

diff -r f8c4e79db153 -r b05cdd060c3e src/HOL/Nominal/Nominal.thy
--- 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 *}
 (*=========================================================*)