# HG changeset patch
# User huffman
# Date 1315858750 25200
# Node ID f05bff62f8a6e3f0d1e5f2642065335d50fbfaa6
# Parent  93943da0a0102b359644f1021bc8573de7eac84e
NEWS and CONTRIBUTORS

diff -r 93943da0a010 -r f05bff62f8a6 CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Sep 12 11:54:20 2011 -0700
+++ b/CONTRIBUTORS	Mon Sep 12 13:19:10 2011 -0700
@@ -7,7 +7,7 @@
 -------------------------------
 
 * September 2011: Peter Gammie
-  Theory HOL/Libary/Saturated: numbers with saturated arithmetic.
+  Theory HOL/Library/Saturated: numbers with saturated arithmetic.
 
 * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
   Refined theory on complete lattices.
@@ -30,6 +30,13 @@
   Theory HOL/Library/Extended_Reals: real numbers extended with
   plus and minus infinity.
 
+* June 2011: Brian Huffman, Portland State University
+  Proof method 'countable_datatype' for theory Library/Countable.
+
+* August 2011: Brian Huffman, Portland State University
+  Misc cleanup of Complex_Main and Multivariate_Analysis.
+
+
 Contributions to Isabelle2011
 -----------------------------
 
diff -r 93943da0a010 -r f05bff62f8a6 NEWS
--- a/NEWS	Mon Sep 12 11:54:20 2011 -0700
+++ b/NEWS	Mon Sep 12 13:19:10 2011 -0700
@@ -98,6 +98,9 @@
 product type 'a * 'b, and provides instance proofs for various order
 and lattice type classes.
 
+* Theory Library/Countable now provides the "countable_datatype" proof
+method for proving "countable" class instances for datatypes.
+
 * Classes bot and top require underlying partial order rather than
 preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
 
@@ -424,6 +427,10 @@
   Now it is defined on the type class {topological_space, comm_monoid_add}.
   Hence it is useable also for extended real numbers.
 
+* Theory Complex_Main: The complex exponential function "expi" is now
+a type-constrained abbreviation for "exp :: complex => complex"; thus
+several polymorphic lemmas about "exp" are now applicable to "expi".
+
 
 *** Document preparation ***