1.1 --- a/NEWS	Mon Jun 14 10:38:28 2010 +0200
     1.2 +++ b/NEWS	Mon Jun 21 11:24:19 2010 +0200
     1.3 @@ -160,15 +160,15 @@
     1.4  'quotient_definition' may be used for defining types and constants by
     1.5  quotient constructions.  An example is the type of integers created by
     1.6  quotienting pairs of natural numbers:
     1.7 -  
     1.8 +
     1.9    fun
    1.10 -    intrel :: "(nat * nat) => (nat * nat) => bool" 
    1.11 +    intrel :: "(nat * nat) => (nat * nat) => bool"
    1.12    where
    1.13      "intrel (x, y) (u, v) = (x + v = u + y)"
    1.14  
    1.15 -  quotient_type int = "nat × nat" / intrel
    1.16 +  quotient_type int = "nat * nat" / intrel
    1.17      by (auto simp add: equivp_def expand_fun_eq)
    1.18 -  
    1.19 +
    1.20    quotient_definition
    1.21      "0::int" is "(0::nat, 0::nat)"
    1.22  
    1.23 @@ -250,6 +250,8 @@
    1.24  * Theory PReal, including the type "preal" and related operations, has
    1.25  been removed.  INCOMPATIBILITY.
    1.26  
    1.27 +* Real: new development using Cauchy Sequences.
    1.28 +
    1.29  * Split off theory "Big_Operators" containing setsum, setprod,
    1.30  Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.
    1.31  
    1.32 @@ -3386,8 +3388,6 @@
    1.33  * Real: proper support for ML code generation, including 'quickcheck'.
    1.34  Reals are implemented as arbitrary precision rationals.
    1.35  
    1.36 -* Real: new development using Cauchy Sequences.
    1.37 -
    1.38  * Hyperreal: Several constants that previously worked only for the
    1.39  reals have been generalized, so they now work over arbitrary vector
    1.40  spaces. Type annotations may need to be added in some cases; potential