--- 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)