| Sat, 04 Jun 2016 16:10:44 +0200 | wenzelm | Integer.lcm normalizes the sign as in HOL/GCD.thy; | file | diff | annotate |
| Wed, 01 Jun 2016 22:35:51 +0200 | wenzelm | proper ceil operation; | file | diff | annotate |
| Wed, 01 Jun 2016 21:31:08 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 01 Jun 2016 19:23:18 +0200 | wenzelm | more adhoc overloading; | file | diff | annotate |
| Wed, 01 Jun 2016 17:46:12 +0200 | wenzelm | clarified exception -- actually reject denominator = 0; | file | diff | annotate |
| Wed, 01 Jun 2016 16:02:02 +0200 | wenzelm | ML pp for Rat.rat; | file | diff | annotate |
| Wed, 01 Jun 2016 15:33:45 +0200 | wenzelm | clarified string_of_rat operations; | file | diff | annotate |
| Wed, 01 Jun 2016 15:19:44 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Wed, 01 Jun 2016 15:17:29 +0200 | wenzelm | clarified signature; | file | diff | annotate |
| Wed, 01 Jun 2016 10:59:57 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Wed, 01 Jun 2016 10:55:10 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 01 Jun 2016 10:45:35 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Tue, 31 May 2016 23:06:03 +0200 | wenzelm | maintain invariant for exported operation; | file | diff | annotate |
| Tue, 31 May 2016 22:39:28 +0200 | wenzelm | prefer more efficient Poly/ML operations, taking care of sign; | file | diff | annotate |
| Tue, 31 May 2016 21:54:10 +0200 | wenzelm | ad-hoc overloading for standard operations on type Rat.rat; | file | diff | annotate |
| Tue, 31 May 2016 19:51:01 +0200 | wenzelm | rat.ML is now part of Pure to allow tigther integration with Isabelle/ML; | file | diff | annotate | base |
| Mon, 04 Jun 2007 11:39:19 +0200 | chaieb | removed fixmes | file | diff | annotate |
| Mon, 04 Jun 2007 11:38:34 +0200 | chaieb | opaque-constraint removed | file | diff | annotate |
| Mon, 21 May 2007 19:11:42 +0200 | haftmann | tuned | file | diff | annotate |
| Sat, 19 May 2007 19:08:06 +0200 | chaieb | added lt and some other infix operation analogous to Ocaml's num library | file | diff | annotate |
| Sun, 13 May 2007 18:15:25 +0200 | haftmann | tuned | file | diff | annotate |
| Tue, 03 Apr 2007 19:24:21 +0200 | wenzelm | avoid overloaded integer constants (accomodate Alice); | file | diff | annotate |
| Fri, 26 Jan 2007 10:22:42 +0100 | paulson | Fixed long-standing, MAJOR bug in "lt" | file | diff | annotate |
| Thu, 04 May 2006 12:50:01 +0200 | webertj | Rat.one added | file | diff | annotate |
| Fri, 21 Oct 2005 14:47:37 +0200 | haftmann | slight corrections | file | diff | annotate |
| Fri, 21 Oct 2005 08:23:45 +0200 | haftmann | added rounding functions | file | diff | annotate |
| Fri, 14 Oct 2005 14:36:39 +0200 | haftmann | added module rat.ML for rational numbers | file | diff | annotate |