# HG changeset patch
# User huffman
# Date 1181682869 -7200
# Node ID 7bb5dc641158b79019ce64ae721084bcc241f15f
# Parent  1517207ec8b9de5f704ecbc65d6e101d1e2bf133
add lemma inj_of_nat

diff -r 1517207ec8b9 -r 7bb5dc641158 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Jun 12 21:59:40 2007 +0200
+++ b/src/HOL/Nat.thy	Tue Jun 12 23:14:29 2007 +0200
@@ -1368,6 +1368,9 @@
 lemma of_nat_eq_0_iff [simp]: "(of_nat m = (0::'a::semiring_char_0)) = (m = 0)"
   by (rule of_nat_eq_iff [of _ 0, simplified])
 
+lemma inj_of_nat: "inj (of_nat :: nat \<Rightarrow> 'a::semiring_char_0)"
+  by (simp add: inj_on_def)
+
 lemma of_nat_diff [simp]:
     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
   by (simp del: of_nat_add