--- 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
-----------------------------
--- 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 ***