#
c554f74b |
|
15-Feb-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Ensure HOL4 works with fixed-width integers under Poly/ML. Integers under Poly/ML 5.6.1 are likely to be fixed-width by default (up until now they've always been arbitrary precision). Some changes were needed to cope with this: - The Arbint and Artbnum structures effectively assumed Int.int = IntInf.int. - The Standard ML structure Time is based on LargeInt.int and not Int.int. Code for printing times has been re-implemented using the Date structure. - The smart-configure.sml file used the Overflow exception to distinguish between Moscow ML and Poly/ML. This test is now based on a difference in the printing of General.Fail exceptions.
|
#
64628539 |
|
05-Jun-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improve error reporting for the Arbnum string parsing functions. Previously Arbnum.fromHexString "g" would raise Option and Arbnum.fromHexString "ag" would return 10. Now both fail with a "String not HEX" message.
|
#
315b2eec |
|
20-Feb-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Slight tuneup for Arbnum.isqrt.
|
#
508be0b4 |
|
20-Feb-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Some basic evaluation support for square roots over ``:num`` and ``:real``. Also add syntax support for transcTheory. Tidied up logrootScript.sml. The evaluation theorems for ``ROOT 2`` were present but they weren't being used. Over the reals a conversion is used -- this will only work for rationals built from perfect squares. For example: > EVAL ``sqrt (9 / 16)`` val it = |- sqrt (9 / 16) = 3 / 4: thm
|
#
8d5fa7fe |
|
26-Jul-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
More assorted code tidying.
|
#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
316436ee |
|
19-Dec-2009 |
Scott Owens <Scott.Owens@cl.cam.ac.uk> |
The PolyML version now uses PolyML's builin IntInf support. (This change doesn't appear to speed up HOL, but it's nice to have anyway.)
|