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