History log of /seL4-l4v-10.1.1/HOL4/src/real/Diff.sml
Revision Date Author Comments
# b4b8e85c 18-Aug-2018 Andreas Lööw <AndreasLoow@users.noreply.github.com>

Don't export ERR from HolKernel


# d4c9027c 16-Dec-2015 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Use lim_grammars in Diff.


# 59d9151a 02-May-2010 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Avoid warning messages when loading realLib under Poly/ML.


# 83b175a9 20-Sep-2009 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Removed a bunch of rarely used functions from hol88Lib. Related documentation
updated.

The ancient hol88 interface should disappear eventually; code using it should
be properly ported to use the current HOL functions instead.


# 6cf562f4 28-Nov-2000 Konrad Slind <konrad.slind@gmail.com>

The reals library builds on Kan.0.


# c64241de 01-Dec-1999 Konrad Slind <konrad.slind@gmail.com>

Minor changes to use "jrhUtils" instead of "useful".


# 0058df84 28-Jun-1999 Michael Norrish <Michael.Norrish@nicta.com.au>

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)


# 58841e67 29-Apr-1999 Michael Norrish <Michael.Norrish@nicta.com.au>

Initial revision