added "fresh_singleton" lemma
authorurbanc
Wed Jan 04 20:20:25 2006 +0100 (2006-01-04)
changeset 1857868420ce82a0b
parent 18577 a636846a02c7
child 18579 002d371401f5
added "fresh_singleton" lemma
src/HOL/Nominal/Nominal.thy
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Jan 04 19:53:39 2006 +0100
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Wed Jan 04 20:20:25 2006 +0100
     1.3 @@ -195,6 +195,10 @@
     1.4    shows "a\<sharp>{}"
     1.5    by (simp add: fresh_def supp_set_empty)
     1.6  
     1.7 +lemma fresh_singleton:
     1.8 +  shows "a\<sharp>{x} = a\<sharp>x"
     1.9 +  by (simp add: fresh_def supp_singleton)
    1.10 +
    1.11  lemma fresh_prod:
    1.12    fixes a :: "'x"
    1.13    and   x :: "'a"