equal
deleted
inserted
replaced
3365 reals into other types. The overloaded constant Reals :: 'a set is now |
3365 reals into other types. The overloaded constant Reals :: 'a set is now |
3366 defined as range of_real; potential INCOMPATIBILITY. |
3366 defined as range of_real; potential INCOMPATIBILITY. |
3367 |
3367 |
3368 * Real: proper support for ML code generation, including 'quickcheck'. |
3368 * Real: proper support for ML code generation, including 'quickcheck'. |
3369 Reals are implemented as arbitrary precision rationals. |
3369 Reals are implemented as arbitrary precision rationals. |
|
3370 |
|
3371 * Real: new development using Cauchy Sequences. |
3370 |
3372 |
3371 * Hyperreal: Several constants that previously worked only for the |
3373 * Hyperreal: Several constants that previously worked only for the |
3372 reals have been generalized, so they now work over arbitrary vector |
3374 reals have been generalized, so they now work over arbitrary vector |
3373 spaces. Type annotations may need to be added in some cases; potential |
3375 spaces. Type annotations may need to be added in some cases; potential |
3374 INCOMPATIBILITY. |
3376 INCOMPATIBILITY. |