src/HOL/NatDef.ML
changeset 11461 ffeac9aa1967
parent 11338 779d289255f7
child 11464 ddea204de5bc
     1.1 --- a/src/HOL/NatDef.ML	Mon Aug 06 12:41:21 2001 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Mon Aug 06 12:42:43 2001 +0200
     1.3 @@ -89,10 +89,9 @@
     1.4  
     1.5  bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
     1.6  
     1.7 -Goal "(!x. x = (0::nat)) = False";
     1.8 +Goal "(ALL x. x = (0::nat)) = False";
     1.9  by Auto_tac;
    1.10  qed "nat_not_singleton";
    1.11 -Addsimps[nat_not_singleton];
    1.12  
    1.13  (*** Basic properties of "less than" ***)
    1.14