1.1 --- a/src/HOL/Int.thy	Sat Sep 03 15:37:41 2011 -0700
     1.2 +++ b/src/HOL/Int.thy	Sat Sep 03 16:00:09 2011 -0700
     1.3 @@ -403,10 +403,6 @@
     1.4  lemma nat_int [simp]: "nat (of_nat n) = n"
     1.5  by (simp add: nat int_def)
     1.6  
     1.7 -(* FIXME: duplicates nat_0 *)
     1.8 -lemma nat_zero [simp]: "nat 0 = 0"
     1.9 -by (simp add: Zero_int_def nat)
    1.10 -
    1.11  lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
    1.12  by (cases z) (simp add: nat le int_def Zero_int_def)
    1.13  
    1.14 @@ -1623,8 +1619,7 @@
    1.15  
    1.16  lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
    1.17  
    1.18 -(* FIXME: duplicates nat_zero *)
    1.19 -lemma nat_0: "nat 0 = 0"
    1.20 +lemma nat_0 [simp]: "nat 0 = 0"
    1.21  by (simp add: nat_eq_iff)
    1.22  
    1.23  lemma nat_1: "nat 1 = Suc 0"