NEWS
changeset 23013 c38c9039dc13
parent 22997 d4f3b015b50b
child 23029 79ee75dc1e59
equal deleted inserted replaced
23012:496b42cf588d 23013:c38c9039dc13
   889 and norm :: 'a => real.
   889 and norm :: 'a => real.
   890 
   890 
   891 * Real: New constant of_real :: real => 'a::real_algebra_1 injects
   891 * Real: New constant of_real :: real => 'a::real_algebra_1 injects
   892 from reals into other types. The overloaded constant Reals :: 'a set
   892 from reals into other types. The overloaded constant Reals :: 'a set
   893 is now defined as range of_real; potential INCOMPATIBILITY.
   893 is now defined as range of_real; potential INCOMPATIBILITY.
       
   894 
       
   895 * Real: ML code generation is supported now and hence also quickcheck.
       
   896 Reals are implemented as arbitrary precision rationals.
   894 
   897 
   895 * Hyperreal: Several constants that previously worked only for the
   898 * Hyperreal: Several constants that previously worked only for the
   896 reals have been generalized, so they now work over arbitrary vector
   899 reals have been generalized, so they now work over arbitrary vector
   897 spaces. Type annotations may need to be added in some cases; potential
   900 spaces. Type annotations may need to be added in some cases; potential
   898 INCOMPATIBILITY.
   901 INCOMPATIBILITY.