theory of saturated naturals contributed by Peter Gammie
authorhaftmann
Wed Sep 07 23:38:52 2011 +0200 (2011-09-07)
changeset 4481827ba81ad0890
parent 44817 b63e445c8f6d
child 44819 fe33d6655186
theory of saturated naturals contributed by Peter Gammie
CONTRIBUTORS
NEWS
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
     1.1 --- a/CONTRIBUTORS	Wed Sep 07 23:07:16 2011 +0200
     1.2 +++ b/CONTRIBUTORS	Wed Sep 07 23:38:52 2011 +0200
     1.3 @@ -6,6 +6,12 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* September 2011: Peter Gammie
     1.8 +  Theory HOL/Libary/Saturated: numbers with saturated arithmetic.
     1.9 +
    1.10 +* August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
    1.11 +  Refined theory on complete lattices.
    1.12 +
    1.13  
    1.14  Contributions to Isabelle2011
    1.15  -----------------------------
     2.1 --- a/NEWS	Wed Sep 07 23:07:16 2011 +0200
     2.2 +++ b/NEWS	Wed Sep 07 23:38:52 2011 +0200
     2.3 @@ -91,6 +91,9 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* Theory Library/Saturated provides type of numbers with saturated
     2.8 +arithmetic.
     2.9 +
    2.10  * Classes bot and top require underlying partial order rather than
    2.11  preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
    2.12  
     3.1 --- a/src/HOL/IsaMakefile	Wed Sep 07 23:07:16 2011 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Wed Sep 07 23:38:52 2011 +0200
     3.3 @@ -463,10 +463,10 @@
     3.4    Library/Quotient_Option.thy Library/Quotient_Product.thy		\
     3.5    Library/Quotient_Sum.thy Library/Quotient_Syntax.thy			\
     3.6    Library/Quotient_Type.thy Library/RBT.thy Library/RBT_Impl.thy	\
     3.7 -  Library/RBT_Mapping.thy Library/README.html Library/Set_Algebras.thy	\
     3.8 -  Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy	\
     3.9 -  Library/Sublist_Order.thy Library/Sum_of_Squares.thy			\
    3.10 -  Library/Sum_of_Squares/sos_wrapper.ML					\
    3.11 +  Library/RBT_Mapping.thy Library/README.html Library/Saturated.thy	\
    3.12 +  Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy	\
    3.13 +  Library/Reflection.thy Library/Sublist_Order.thy			\
    3.14 +  Library/Sum_of_Squares.thy Library/Sum_of_Squares/sos_wrapper.ML	\
    3.15    Library/Sum_of_Squares/sum_of_squares.ML				\
    3.16    Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
    3.17    Library/Wfrec.thy Library/While_Combinator.thy Library/Zorn.thy	\
     4.1 --- a/src/HOL/Library/Library.thy	Wed Sep 07 23:07:16 2011 +0200
     4.2 +++ b/src/HOL/Library/Library.thy	Wed Sep 07 23:38:52 2011 +0200
     4.3 @@ -55,6 +55,7 @@
     4.4    Ramsey
     4.5    Reflection
     4.6    RBT_Mapping
     4.7 +  Saturated
     4.8    Set_Algebras
     4.9    State_Monad
    4.10    Sum_of_Squares