changeset 20388 | b5a61270ea5a |
parent 19986 | 3e0eababf58d |
child 20809 | 6c4fd0b4b63a |
--- a/src/HOL/Nominal/Nominal.thy Mon Aug 14 13:47:00 2006 +0200 +++ b/src/HOL/Nominal/Nominal.thy Wed Aug 16 16:44:41 2006 +0200 @@ -224,6 +224,12 @@ apply(simp add: supp_def perm_int_def) done +lemma supp_nat: + fixes n::"nat" + shows "supp (n) = {}" + apply(simp add: supp_def perm_nat_def) + done + lemma supp_char: fixes c::"char" shows "supp (c) = {}"