History log of /seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/variableScript.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.


# 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
----------------------------------------------------------------------