*** empty log message ***
authornipkow
Sat, 19 May 2007 07:47:51 +0200
changeset 23013 c38c9039dc13
parent 23012 496b42cf588d
child 23014 00d8bf2fce42
*** empty log message ***
NEWS
--- a/NEWS	Sat May 19 04:52:24 2007 +0200
+++ b/NEWS	Sat May 19 07:47:51 2007 +0200
@@ -892,6 +892,9 @@
 from reals into other types. The overloaded constant Reals :: 'a set
 is now defined as range of_real; potential INCOMPATIBILITY.
 
+* Real: ML code generation is supported now and hence also quickcheck.
+Reals are implemented as arbitrary precision rationals.
+
 * 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