# HG changeset patch
# User wenzelm
# Date 1277112259 -7200
# Node ID 35815ce9218a8822a50f5d80b96aa8d1970ec35d
# Parent  f23e60581eb361261b6e70d4587bea0047fab195
final tuning;

diff -r f23e60581eb3 -r 35815ce9218a NEWS
--- a/NEWS	Mon Jun 14 10:38:28 2010 +0200
+++ b/NEWS	Mon Jun 21 11:24:19 2010 +0200
@@ -160,15 +160,15 @@
 'quotient_definition' may be used for defining types and constants by
 quotient constructions.  An example is the type of integers created by
 quotienting pairs of natural numbers:
-  
+
   fun
-    intrel :: "(nat * nat) => (nat * nat) => bool" 
+    intrel :: "(nat * nat) => (nat * nat) => bool"
   where
     "intrel (x, y) (u, v) = (x + v = u + y)"
 
-  quotient_type int = "nat × nat" / intrel
+  quotient_type int = "nat * nat" / intrel
     by (auto simp add: equivp_def expand_fun_eq)
-  
+
   quotient_definition
     "0::int" is "(0::nat, 0::nat)"
 
@@ -250,6 +250,8 @@
 * Theory PReal, including the type "preal" and related operations, has
 been removed.  INCOMPATIBILITY.
 
+* Real: new development using Cauchy Sequences.
+
 * Split off theory "Big_Operators" containing setsum, setprod,
 Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.
 
@@ -3386,8 +3388,6 @@
 * Real: proper support for ML code generation, including 'quickcheck'.
 Reals are implemented as arbitrary precision rationals.
 
-* Real: new development using Cauchy Sequences.
-
 * Hyperreal: Several constants that previously worked only for the
 reals have been generalized, so they now work over arbitrary vector
 spaces. Type annotations may need to be added in some cases; potential