src/HOL/Nat.thy
changeset 32456 341c83339aeb
parent 32437 66f1a0dfe7d9
child 32772 50d090ca93f8
     1.1 --- a/src/HOL/Nat.thy	Sat Aug 29 14:31:39 2009 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon Aug 31 14:09:42 2009 +0200
     1.3 @@ -1588,9 +1588,6 @@
     1.4  lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
     1.5    using inc_induct[of 0 k P] by blast
     1.6  
     1.7 -lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
     1.8 -  by auto
     1.9 -
    1.10  (*The others are
    1.11        i - j - k = i - (j + k),
    1.12        k \<le> j ==> j - k + i = j + i - k,