added missing supp_nat lemma
authorurbanc
Wed, 16 Aug 2006 16:44:41 +0200
changeset 20388 b5a61270ea5a
parent 20387 6c0ef1c77c7b
child 20389 8b6ecb22ef35
added missing supp_nat lemma
src/HOL/Nominal/Nominal.thy
--- 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) = {}"