History log of /seL4-l4v-10.1.1/HOL4/src/ring/src/quote.sml
Revision Date Author Comments
# 2554535e 09-Oct-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Make references private in src/ring/src/quote.sml


# f3b2bd23 09-Oct-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Give src/ring/src/quote a signature


# 74e79f0e 06-Sep-2018 Fabian Immler <immler@in.tum.de>

avoid ref-match


# 6a81a039 21-May-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Remove TABs from src

Will also make selftest to check that they aren't introduced


# 95d60bd3 02-Oct-2017 Michael Norrish <Michael.Norrish@nicta.com.au>

Remove -- as an alias for Term parser.

As per comment in release notes this has long been replaced as
appropriate style.


# 4761143b 10-Aug-2009 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!


# 6a6e7dda 19-Oct-2003 Joe Hurd <joe@gilith.com>

Made a bunch of changes to the HOL source to make it more "Standard ML",
to make it easier to port to MLton.

For example:
+ Added lots of structure wrappers around miscellaneous .sml files.
+ The type of "before" is 'a * () -> 'a, not 'a * 'b -> 'a, as Moscow ML
currently thinks.
+ Added "val _ = " before random declarations.

A plea: if I'm ever going to succeed in porting HOL to MLton, could
people please stop using Polyhash. It's very useful, but there's
nothing like it in MLton (or indeed Standard ML). In theory I'm going
to have to change the (sometimes complicated) code to use Binarymap or
something like it, but in practice I'll only do that when there's
absolutely no other way.


# 48171fb6 30-Nov-2000 Konrad Slind <konrad.slind@gmail.com>

src/ring now builds in Kan.0.


# 3c25614c 18-Oct-1999 Bruno Barras <barras@lix.polytechnique.fr>

added the ring library