src/HOL/Nominal/Nominal.thy
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) = {}"