removed an unsuitable default simprule
authorpaulson
Mon Aug 06 12:42:43 2001 +0200 (2001-08-06)
changeset 11461ffeac9aa1967
parent 11460 e5fb885bfe3a
child 11462 cf3e7f5ad0e1
removed an unsuitable default simprule
src/HOL/Library/Continuity.thy
src/HOL/NatDef.ML
     1.1 --- a/src/HOL/Library/Continuity.thy	Mon Aug 06 12:41:21 2001 +0200
     1.2 +++ b/src/HOL/Library/Continuity.thy	Mon Aug 06 12:42:43 2001 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4     apply (rule up_chainI)
     1.5     apply  simp+
     1.6    apply (drule Un_absorb1)
     1.7 -  apply auto
     1.8 +  apply (auto simp add: nat_not_singleton)
     1.9    done
    1.10  
    1.11  
    1.12 @@ -110,7 +110,7 @@
    1.13     apply (rule down_chainI)
    1.14     apply simp+
    1.15    apply (drule Int_absorb1)
    1.16 -  apply auto
    1.17 +  apply (auto simp add: nat_not_singleton)
    1.18    done
    1.19  
    1.20  
     2.1 --- a/src/HOL/NatDef.ML	Mon Aug 06 12:41:21 2001 +0200
     2.2 +++ b/src/HOL/NatDef.ML	Mon Aug 06 12:42:43 2001 +0200
     2.3 @@ -89,10 +89,9 @@
     2.4  
     2.5  bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
     2.6  
     2.7 -Goal "(!x. x = (0::nat)) = False";
     2.8 +Goal "(ALL x. x = (0::nat)) = False";
     2.9  by Auto_tac;
    2.10  qed "nat_not_singleton";
    2.11 -Addsimps[nat_not_singleton];
    2.12  
    2.13  (*** Basic properties of "less than" ***)
    2.14