--- 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 \
--- a/src/HOL/Library/Library.thy Wed Sep 07 23:07:16 2011 +0200
+++ b/src/HOL/Library/Library.thy Wed Sep 07 23:38:52 2011 +0200
@@ -55,6 +55,7 @@
Ramsey
Reflection
RBT_Mapping
+ Saturated
Set_Algebras
State_Monad
Sum_of_Squares