author | urbanc |
Wed, 16 Aug 2006 16:44:41 +0200 | |
changeset 20388 | b5a61270ea5a |
parent 20387 | 6c0ef1c77c7b |
child 20389 | 8b6ecb22ef35 |
--- 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) = {}"