# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1283518125 -28800
# Node ID 937b6088a3a069c1ebe82583a50e1ec81e6157af
# Parent  86028b2016bd60e35b9d5d539c1fecfc6dce8629
added supp_set lemma

diff -r 86028b2016bd -r 937b6088a3a0 Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Thu Sep 02 18:10:06 2010 +0800
+++ b/Nominal-General/Nominal2_Supp.thy	Fri Sep 03 20:48:45 2010 +0800
@@ -543,5 +543,12 @@
   using fin
   by (simp add: supp_of_fin_sets)
 
+lemma supp_set:
+  fixes xs :: "('a::fs) list"
+  shows "supp (set xs) = supp xs"
+apply(induct xs)
+apply(simp add: supp_set_empty supp_Nil)
+apply(simp add: supp_Cons finite_set supp_of_fin_insert)
+done
 
 end