# HG changeset patch
# User oheimb
# Date 991320614 -7200
# Node ID 779d289255f7ee98290e91e1d8698fce54e65feb
# Parent  9d6d6a8966b91bdf8a8e178943f47864336224f4
added nat_not_singleton (also to simpset)

diff -r 9d6d6a8966b9 -r 779d289255f7 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Thu May 31 16:50:13 2001 +0200
+++ b/src/HOL/NatDef.ML	Thu May 31 16:50:14 2001 +0200
@@ -89,6 +89,11 @@
 
 bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
 
+Goal "(!x. x = (0::nat)) = False";
+by Auto_tac;
+qed "nat_not_singleton";
+Addsimps[nat_not_singleton];
+
 (*** Basic properties of "less than" ***)
 
 Goalw [wf_def, pred_nat_def] "wf pred_nat";