History log of /seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/barendregt.sml
Revision Date Author Comments
# 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!


# c20e5e83 24-Jun-2005 Peter Homeier <palantir@trustworthytools.com>

----------------------------------------------------------------------

Committing in a revised version of the quotients package, where now
erroneous input theorems are usually detected early, and the erroneous
theorem listed in an error message. This should greatly improve the
usability of the package, especially for new users. Thanks to Michael
Norrish for prodding me on this one.

Also added a new version of finite sets from lists, due to Michael Norrish.

Also moved the "obj" directory to now be called "sigma"; this contains
the sigma calculus example from Abadi and Cardelli, as described in the
longer 45-page paper.

Modified Files:
hol98/src/quotient/examples/finite_setScript.sml
hol98/src/quotient/src/quotient.sml
hol98/src/quotient/src/quotientScript.sml
Added Files:
hol98/src/quotient/examples/ext_finite_setScript.sml
hol98/src/quotient/examples/sigma/MutualIndThen.sig
hol98/src/quotient/examples/sigma/MutualIndThen.sml
hol98/src/quotient/examples/sigma/alphaScript.sml
hol98/src/quotient/examples/sigma/barendregt.sig
hol98/src/quotient/examples/sigma/barendregt.sml
hol98/src/quotient/examples/sigma/ind_rel.sig
hol98/src/quotient/examples/sigma/ind_rel.sml
hol98/src/quotient/examples/sigma/liftScript.sml
hol98/src/quotient/examples/sigma/more_listScript.sml
hol98/src/quotient/examples/sigma/more_setScript.sml
hol98/src/quotient/examples/sigma/objectScript.sml
hol98/src/quotient/examples/sigma/reductionScript.sml
hol98/src/quotient/examples/sigma/semanticsScript.sml
hol98/src/quotient/examples/sigma/tactics.sig
hol98/src/quotient/examples/sigma/tactics.sml
hol98/src/quotient/examples/sigma/variableScript.sml
Removed Files:
hol98/src/quotient/examples/obj/MutualIndThen.sig
hol98/src/quotient/examples/obj/MutualIndThen.sml
hol98/src/quotient/examples/obj/alphaScript.sml
hol98/src/quotient/examples/obj/barendregt.sig
hol98/src/quotient/examples/obj/barendregt.sml
hol98/src/quotient/examples/obj/ind_rel.sig
hol98/src/quotient/examples/obj/ind_rel.sml
hol98/src/quotient/examples/obj/liftScript.sml
hol98/src/quotient/examples/obj/more_listScript.sml
hol98/src/quotient/examples/obj/more_setScript.sml
hol98/src/quotient/examples/obj/objectScript.sml
hol98/src/quotient/examples/obj/reductionScript.sml
hol98/src/quotient/examples/obj/semanticsScript.sml
hol98/src/quotient/examples/obj/tactics.sig
hol98/src/quotient/examples/obj/tactics.sml
hol98/src/quotient/examples/obj/variableScript.sml
----------------------------------------------------------------------