Summary
- merged
- NEWS;
- more adhoc overloading; eliminated pointless Rat.eq: this is an equality type; tuned;
- clarified exception -- actually reject denominator = 0;
- ML pp for Rat.rat;
- clarified string_of_rat operations;
- tuned signature;
- clarified signature;
- prefer rat numberals;
- support rat numerals via special antiquotation syntax;
- tuned signature;
- tuned;
- tuned signature;
- maintain invariant for exported operation;
- prefer more efficient Poly/ML operations, taking care of sign;
- ad-hoc overloading for standard operations on type Rat.rat;
- rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;