#
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.
|
#
0bbd2a7e |
|
21-Jun-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix. 90+% of this work was done by Ramana Kumar. The following list are the commits for a series of individual commits that have been squished into one big change: * remove mention of TruePrefix from the add_rule docfile * first batch of changes removing TruePrefix from src/parse * replace TruePrefix by Prefix in boolScript.sml * remove TruePrefix from Rsyntax is a fixity ever required for new_specification? * some more Prefix -> NONE and TruePrefix -> Prefix in theories * TruePrefix changes for datatype * TruePrefix changes for res_quan * TruePrefix->Prefix in a TeX selftest * TruePrefix changes for quotient * TruePrefix changes for integer and real * fix quotient examples for TruePrefix removal * more fixes for quotient examples * fixes for lambda example for TruePrefix removal * Reword description manual in light of removal of TruePrefix. * Fix msgTheory quotient example; Poly 5.3 had problems with monotypes. * Fixes for files in examples/lambda given removal of TruePrefix. * Fix in examples/unification given removal of TruePrefix. * Fix in examples/HolCheck given removal of TruePrefix. * Fixes in examples/acl2 given removal of TruePrefix.
|
#
d9003833 |
|
26-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fairly dramatic change, supporting the use of "syntactic patterns". It is now possible to overload a name to term (typically a lambda-abstraction) in order to create syntax-only definitions. For example, there is a definition of not-equals now in the system: val _ = overload_on ("<>", ``\x y. ~(x = y)``) val _ = set_fixity "<>" (Infix(NONASSOC, 450)) This definition is parsed and pretty-printed. Two other annoying changes. The interface for adding unicode variants has changed, and I have made precedence level 450 of the parser non-associative. This latter change has caused most of the (minor) adjustments to the files below. The regression test doesn't go through yet. (Currently there is a failure in quotient/examples/sigma that I don't understand.)
|
#
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 ----------------------------------------------------------------------
|