| #
438cc573 |
|
20-Aug-2019 |
wenzelm <none@none> |
clarified signature;
|
| #
b193b20b |
|
04-Jun-2016 |
wenzelm <none@none> |
Integer.lcm normalizes the sign as in HOL/GCD.thy;
tuned;
|
| #
5571e029 |
|
01-Jun-2016 |
wenzelm <none@none> |
proper ceil operation;
|
| #
024e69dc |
|
01-Jun-2016 |
wenzelm <none@none> |
tuned;
|
| #
e31b651f |
|
01-Jun-2016 |
wenzelm <none@none> |
more adhoc overloading;
eliminated pointless Rat.eq: this is an equality type;
tuned;
|
| #
887e097e |
|
01-Jun-2016 |
wenzelm <none@none> |
clarified exception -- actually reject denominator = 0;
|
| #
1968198b |
|
01-Jun-2016 |
wenzelm <none@none> |
ML pp for Rat.rat;
|
| #
a6711317 |
|
01-Jun-2016 |
wenzelm <none@none> |
clarified string_of_rat operations;
|
| #
aabf9b9f |
|
01-Jun-2016 |
wenzelm <none@none> |
tuned signature;
|
| #
8b8daeff |
|
01-Jun-2016 |
wenzelm <none@none> |
clarified signature;
|
| #
4b5f8f15 |
|
01-Jun-2016 |
wenzelm <none@none> |
tuned signature;
|
| #
4c033760 |
|
01-Jun-2016 |
wenzelm <none@none> |
tuned;
|
| #
833e5446 |
|
01-Jun-2016 |
wenzelm <none@none> |
tuned signature;
|
| #
ef55200b |
|
31-May-2016 |
wenzelm <none@none> |
maintain invariant for exported operation;
|
| #
80ac26e2 |
|
31-May-2016 |
wenzelm <none@none> |
prefer more efficient Poly/ML operations, taking care of sign;
|
| #
134619e9 |
|
31-May-2016 |
wenzelm <none@none> |
ad-hoc overloading for standard operations on type Rat.rat;
|
| #
ca5b4b9a |
|
31-May-2016 |
wenzelm <none@none> |
rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;
--HG--
rename : src/Tools/rat.ML => src/Pure/General/rat.ML
|
| #
a60ae8f8 |
|
04-Jun-2007 |
chaieb <none@none> |
removed fixmes
|
| #
6f8c7c98 |
|
04-Jun-2007 |
chaieb <none@none> |
opaque-constraint removed
|
| #
a3c18bb0 |
|
21-May-2007 |
haftmann <none@none> |
tuned
|
| #
3d494327 |
|
19-May-2007 |
chaieb <none@none> |
added lt and some other infix operation analogous to Ocaml's num library
|
| #
c2a01431 |
|
13-May-2007 |
haftmann <none@none> |
tuned
|
| #
866c98bc |
|
03-Apr-2007 |
wenzelm <none@none> |
avoid overloaded integer constants (accomodate Alice);
|
| #
84dea1f6 |
|
26-Jan-2007 |
paulson <none@none> |
Fixed long-standing, MAJOR bug in "lt"
|
| #
21be3548 |
|
03-May-2006 |
webertj <none@none> |
Rat.one added
|
| #
1d5a9cd9 |
|
21-Oct-2005 |
haftmann <none@none> |
slight corrections
|
| #
6399ab42 |
|
21-Oct-2005 |
haftmann <none@none> |
added rounding functions
|
| #
259ba3bc |
|
14-Oct-2005 |
haftmann <none@none> |
added module rat.ML for rational numbers
|