--- a/src/HOL/Nominal/Nominal.thy Sun May 20 10:13:06 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Sun May 20 13:39:46 2007 +0200
@@ -150,7 +150,12 @@
(* permutation on characters (used in strings) *)
defs (unchecked overloaded)
- perm_char_def: "pi\<bullet>(s::char) \<equiv> s"
+ perm_char_def: "pi\<bullet>(c::char) \<equiv> c"
+
+lemma perm_string:
+ fixes s::"string"
+ shows "pi\<bullet>s = s"
+by (induct s)(auto simp add: perm_char_def)
(* permutation on ints *)
defs (unchecked overloaded)
@@ -272,8 +277,7 @@
lemma supp_string:
fixes s::"string"
shows "supp (s) = {}"
-apply(induct s)
-apply(auto simp add: supp_char supp_list_nil supp_list_cons)
+apply(simp add: supp_def perm_string)
done
lemma fresh_set_empty: