# HG changeset patch
# User huffman
# Date 1315090809 25200
# Node ID 075327b8e841f68acf2c864c50e42435a97940cd
# Parent  cad98c8f0e356747881df79e4c58c2f64acfc9e6
remove duplicate lemma nat_zero in favor of nat_0

diff -r cad98c8f0e35 -r 075327b8e841 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sat Sep 03 15:37:41 2011 -0700
+++ b/src/HOL/Int.thy	Sat Sep 03 16:00:09 2011 -0700
@@ -403,10 +403,6 @@
 lemma nat_int [simp]: "nat (of_nat n) = n"
 by (simp add: nat int_def)
 
-(* FIXME: duplicates nat_0 *)
-lemma nat_zero [simp]: "nat 0 = 0"
-by (simp add: Zero_int_def nat)
-
 lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
 by (cases z) (simp add: nat le int_def Zero_int_def)
 
@@ -1623,8 +1619,7 @@
 
 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
 
-(* FIXME: duplicates nat_zero *)
-lemma nat_0: "nat 0 = 0"
+lemma nat_0 [simp]: "nat 0 = 0"
 by (simp add: nat_eq_iff)
 
 lemma nat_1: "nat 1 = Suc 0"