# HG changeset patch
# User huffman
# Date 1268838684 25200
# Node ID a50237ec0ecd3314417ebd5f9488db5c2e66a460
# Parent  1ed86128316cbea8a18b77637e0549e7224789f9
NEWS: Nat_Bijection library

diff -r 1ed86128316c -r a50237ec0ecd NEWS
--- a/NEWS	Wed Mar 17 12:21:54 2010 +0100
+++ b/NEWS	Wed Mar 17 08:11:24 2010 -0700
@@ -221,6 +221,40 @@
 * Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid
 clash with new theory Quotient in Main HOL.
 
+* Library/Nat_Bijection.thy is a collection of bijective functions
+between nat and other types, which supersedes the older libraries
+Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy.  INCOMPATIBILITY.
+
+  Constants:
+  Nat_Int_Bij.nat2_to_nat         ~> prod_encode
+  Nat_Int_Bij.nat_to_nat2         ~> prod_decode
+  Nat_Int_Bij.int_to_nat_bij      ~> int_encode
+  Nat_Int_Bij.nat_to_int_bij      ~> int_decode
+  Countable.pair_encode           ~> prod_encode
+  NatIso.prod2nat                 ~> prod_encode
+  NatIso.nat2prod                 ~> prod_decode
+  NatIso.sum2nat                  ~> sum_encode
+  NatIso.nat2sum                  ~> sum_decode
+  NatIso.list2nat                 ~> list_encode
+  NatIso.nat2list                 ~> list_decode
+  NatIso.set2nat                  ~> set_encode
+  NatIso.nat2set                  ~> set_decode
+
+  Lemmas:
+  Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_decode
+  Nat_Int_Bij.nat2_to_nat_inj     ~> inj_prod_encode
+  Nat_Int_Bij.nat2_to_nat_surj    ~> surj_prod_encode
+  Nat_Int_Bij.nat_to_nat2_inj     ~> inj_prod_decode
+  Nat_Int_Bij.nat_to_nat2_surj    ~> surj_prod_decode
+  Nat_Int_Bij.i2n_n2i_id          ~> int_encode_inverse
+  Nat_Int_Bij.n2i_i2n_id          ~> int_decode_inverse
+  Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode
+  Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode
+  Nat_Int_Bij.inj_nat_to_int_bij  ~> inj_int_encode
+  Nat_Int_Bij.inj_int_to_nat_bij  ~> inj_int_decode
+  Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode
+  Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode
+
 
 *** ML ***