# HG changeset patch
# User urbanc
# Date 1136402425 -3600
# Node ID 68420ce82a0b6e5ff7cca67acb772ffe47a58925
# Parent  a636846a02c754925019ad25c25c144ae690f091
added "fresh_singleton" lemma

diff -r a636846a02c7 -r 68420ce82a0b src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Jan 04 19:53:39 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Jan 04 20:20:25 2006 +0100
@@ -195,6 +195,10 @@
   shows "a\<sharp>{}"
   by (simp add: fresh_def supp_set_empty)
 
+lemma fresh_singleton:
+  shows "a\<sharp>{x} = a\<sharp>x"
+  by (simp add: fresh_def supp_singleton)
+
 lemma fresh_prod:
   fixes a :: "'x"
   and   x :: "'a"