# HG changeset patch
# User paulson
# Date 997094563 -7200
# Node ID ffeac9aa1967bd9b3fd94840411811f8afedb296
# Parent  e5fb885bfe3aafbade9274f67924e24287e56efa
removed an unsuitable default simprule

diff -r e5fb885bfe3a -r ffeac9aa1967 src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Mon Aug 06 12:41:21 2001 +0200
+++ b/src/HOL/Library/Continuity.thy	Mon Aug 06 12:42:43 2001 +0200
@@ -82,7 +82,7 @@
    apply (rule up_chainI)
    apply  simp+
   apply (drule Un_absorb1)
-  apply auto
+  apply (auto simp add: nat_not_singleton)
   done
 
 
@@ -110,7 +110,7 @@
    apply (rule down_chainI)
    apply simp+
   apply (drule Int_absorb1)
-  apply auto
+  apply (auto simp add: nat_not_singleton)
   done
 
 
diff -r e5fb885bfe3a -r ffeac9aa1967 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Mon Aug 06 12:41:21 2001 +0200
+++ b/src/HOL/NatDef.ML	Mon Aug 06 12:42:43 2001 +0200
@@ -89,10 +89,9 @@
 
 bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
 
-Goal "(!x. x = (0::nat)) = False";
+Goal "(ALL x. x = (0::nat)) = False";
 by Auto_tac;
 qed "nat_not_singleton";
-Addsimps[nat_not_singleton];
 
 (*** Basic properties of "less than" ***)