# HG changeset patch
# User urbanc
# Date 1136856730 -3600
# Node ID f0acb66858b4703820e8336f3044953b8cd33188
# Parent  b6596f579e4037f399f0033ae46b5f4fa7841f65
added the lemmas supp_char and supp_string

diff -r b6596f579e40 -r f0acb66858b4 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Jan 09 15:55:15 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Tue Jan 10 02:32:10 2006 +0100
@@ -203,6 +203,19 @@
   apply(simp add: supp_def perm_int_def)
   done
 
+lemma supp_char:
+  fixes c::"char"
+  shows "supp (c) = {}"
+  apply(simp add: supp_def perm_char_def)
+  done
+  
+lemma supp_string:
+  fixes s::"string"
+  shows "supp (s) = {}"
+apply(induct s)
+apply(auto simp add: supp_char supp_list_nil supp_list_cons)
+done
+
 lemma fresh_set_empty:
   shows "a\<sharp>{}"
   by (simp add: fresh_def supp_set_empty)