equal
deleted
inserted
replaced
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. 