# HG changeset patch
# User nipkow
# Date 1249920775 -7200
# Node ID e73eb2db47274969c84e59ddab68c799f579fd85
# Parent  7887cb2848bbe6b73fc8489e68601a1c25a9f040
added bij lemmas

diff -r 7887cb2848bb -r e73eb2db4727 src/HOL/Library/Nat_Int_Bij.thy
--- a/src/HOL/Library/Nat_Int_Bij.thy	Mon Aug 10 17:00:41 2009 +0200
+++ b/src/HOL/Library/Nat_Int_Bij.thy	Mon Aug 10 18:12:55 2009 +0200
@@ -165,5 +165,11 @@
 lemma inj_int_to_nat_bij: "inj int_to_nat_bij"
 by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)
 
+lemma bij_nat_to_int_bij: "bij nat_to_int_bij"
+by(simp add:bij_def inj_nat_to_int_bij surj_nat_to_int_bij)
+
+lemma bij_int_to_nat_bij: "bij int_to_nat_bij"
+by(simp add:bij_def inj_int_to_nat_bij surj_int_to_nat_bij)
+
 
 end