summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Mon, 12 Sep 2011 13:19:10 -0700 | |

changeset 44908 | f05bff62f8a6 |

parent 44907 | 93943da0a010 |

child 44909 | 1f5d6eb73549 |

NEWS and CONTRIBUTORS

CONTRIBUTORS | file | annotate | diff | comparison | revisions | |

NEWS | file | annotate | diff | comparison | revisions |

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