added nat_not_singleton (also to simpset)

--- 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";