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

author | haftmann |

Wed, 07 Sep 2011 23:38:52 +0200 | |

changeset 44818 | 27ba81ad0890 |

parent 44817 | b63e445c8f6d |

child 44819 | fe33d6655186 |

theory of saturated naturals contributed by Peter Gammie

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

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

src/HOL/IsaMakefile | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Library.thy | file | annotate | diff | comparison | revisions |

--- a/CONTRIBUTORS Wed Sep 07 23:07:16 2011 +0200 +++ b/CONTRIBUTORS Wed Sep 07 23:38:52 2011 +0200 @@ -6,6 +6,12 @@ Contributions to this Isabelle version -------------------------------------- +* September 2011: Peter Gammie + Theory HOL/Libary/Saturated: numbers with saturated arithmetic. + +* August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM + Refined theory on complete lattices. + Contributions to Isabelle2011 -----------------------------

--- a/NEWS Wed Sep 07 23:07:16 2011 +0200 +++ b/NEWS Wed Sep 07 23:38:52 2011 +0200 @@ -91,6 +91,9 @@ *** HOL *** +* Theory Library/Saturated provides type of numbers with saturated +arithmetic. + * Classes bot and top require underlying partial order rather than preorder: uniqueness of bot and top is guaranteed. INCOMPATIBILITY.

--- a/src/HOL/IsaMakefile Wed Sep 07 23:07:16 2011 +0200 +++ b/src/HOL/IsaMakefile Wed Sep 07 23:38:52 2011 +0200 @@ -463,10 +463,10 @@ Library/Quotient_Option.thy Library/Quotient_Product.thy \ Library/Quotient_Sum.thy Library/Quotient_Syntax.thy \ Library/Quotient_Type.thy Library/RBT.thy Library/RBT_Impl.thy \ - Library/RBT_Mapping.thy Library/README.html Library/Set_Algebras.thy \ - Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy \ - Library/Sublist_Order.thy Library/Sum_of_Squares.thy \ - Library/Sum_of_Squares/sos_wrapper.ML \ + Library/RBT_Mapping.thy Library/README.html Library/Saturated.thy \ + Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \ + Library/Reflection.thy Library/Sublist_Order.thy \ + Library/Sum_of_Squares.thy Library/Sum_of_Squares/sos_wrapper.ML \ Library/Sum_of_Squares/sum_of_squares.ML \ Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \ Library/Wfrec.thy Library/While_Combinator.thy Library/Zorn.thy \