#
54650888 |
|
02-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix quotient/examples/{lambda,sigma} given tight equality
|
#
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.
|
#
0d994131 |
|
30-Jul-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Clean quotient examples: now use core Mutual lib, rather than own copy This is a start, of sorts, on having a go at github issue #10
|
#
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!
|
#
0ca12743 |
|
26-Apr-2007 |
Peter Homeier <palantir@trustworthytools.com> |
---------------------------------------------------------------------- Committing in revised versions of the quotient examples. The change from (. => . | .) to (if . then . else .) caused the old versions to break. Modified Files: lambda/alphaScript.sml lambda/termScript.sml lambda/variableScript.sml sigma/alphaScript.sml sigma/objectScript.sml sigma/variableScript.sml ----------------------------------------------------------------------
|
#
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 ----------------------------------------------------------------------
|