--- 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