# HG changeset patch
# User haftmann
# Date 1315431532 -7200
# Node ID 27ba81ad08908d3d785342fc6d557e5ba3de37a2
# Parent  b63e445c8f6db04f791bf95c112aa94d1018cea7
theory of saturated naturals contributed by Peter Gammie

diff -r b63e445c8f6d -r 27ba81ad0890 CONTRIBUTORS
--- 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
 -----------------------------
diff -r b63e445c8f6d -r 27ba81ad0890 NEWS
--- 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.
 
diff -r b63e445c8f6d -r 27ba81ad0890 src/HOL/IsaMakefile
--- 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	\
diff -r b63e445c8f6d -r 27ba81ad0890 src/HOL/Library/Library.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