#
7843d690 |
|
24-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix pretty-printing of real and relation inverses Now both get to keep their pretty superscript forms (-1 for the reals, and T for the relations) even when both theories are loaded. The cost is that neither will be printed as "inv" when unapplied to arguments, instead appearing as "realinv" and "relinv" respectively. Closes #481
|
#
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.
|
#
25df2e1a |
|
31-Oct-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add rule for "inv" in realaxTheory. Previously the superscript T rule from relationTheory was active.
|
#
94b064b9 |
|
15-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove unnecessary structure bracketting As per 89fc99bc3, but on as many examples as a grep -R can find.
|
#
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.
|
#
52fb1be0 |
|
21-Sep-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed further functions from hol88Lib.
|
#
d653fb1c |
|
11-Feb-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement unary minus (the old ~ still also works). Selftest level 2 passes. Changes in the "words world" were replacing $- with -. In the two quotient changes, I made sure that the infix operator that used the - character was part of the grammar before it was parsed. This is necessary because - is now a non-aggregating character, mainly so that ``--p`` parses as three tokens, not two. Of course, if you added -- to your grammar, then it would go back to parsing as two.
|
#
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.)
|
#
f33e0630 |
|
05-Mar-2007 |
Joe Hurd <joe@gilith.com> |
Did some community service expunging all occurrences of the old syntax for if-then-else from the HOL distribution. Apologies if I've broken your example or development: you can either upgrade it to use the new syntax or else issue the magic parser incantation that I chopped out of boolScript.sml on this check in.
|
#
81127fc1 |
|
01-Apr-2005 |
Peter Homeier <palantir@trustworthytools.com> |
---------------------------------------------------------------------- Enter Log. Lines beginning with `CVS:' are removed automatically Committing in a revision to the quotients library, with associated corrections to the dependent libraries. Added a feature requested by Michael Norrish, that the tool generate trivial respectfulness theorems if the user leaves them out, of the form !x y. (x = y) ==> (treal_of_hreal x) treal_eq (treal_of_hreal y) where the relation is a true equivalence relation, i.e., reflexive. This enabled the deletion of three trivial respectfulness theorems that I had added when moving the dependent libraries to use the new quotient tool. Harrison's tool had not required these, because his system only dealt with true equivalence relations, which are always reflexive, so in the above example, the respectfulness of treal_of_hreal was easy to prove. Also added a feature to check that all of the constants being lifted are properly represented by respectfulness theorems. This is only sensible, and should catch a simple and common user error. Also divided the quotientScript.sml file into five, adding four new files for the four type operators "list", "option", "pair", and "sum". Each has the definitions and theorems appropriate for that type operator, and for some of the common constants associated with the type operator. Also added quotientLib.sml, which includes all the others. Thus a user can easily get everything in the quotient library by simply typing "open quotientLib;". Modified Files: hol98/src/integer/integerScript.sml hol98/src/n_bit/wordFunctor.sml hol98/src/quotient/src/quotient.sig hol98/src/quotient/src/quotient.sml hol98/src/quotient/src/quotientScript.sml hol98/src/real/hratScript.sml hol98/src/real/realaxScript.sml Added Files: hol98/src/quotient/src/quotientLib.sml hol98/src/quotient/src/quotient_listScript.sml hol98/src/quotient/src/quotient_optionScript.sml hol98/src/quotient/src/quotient_pairScript.sml hol98/src/quotient/src/quotient_sumScript.sml ----------------------------------------------------------------------
|
#
af0eca2b |
|
17-Mar-2005 |
Peter Homeier <palantir@trustworthytools.com> |
---------------------------------------------------------------------- Committing in src/real/realaxScript.sml. I left a small extra "handle e => Raise e" in the file, which is not needed. This update just cleans that out. Modified Files: hol98/src/real/realaxScript.sml ----------------------------------------------------------------------
|
#
bd417ac8 |
|
17-Mar-2005 |
Peter Homeier <palantir@trustworthytools.com> |
---------------------------------------------------------------------- Edited the "real" library to use the new quotient library. The hrealScript.sml and realScript.sml files only had a mention of EquivType in a comment, not for actual use; these have been deleted. The hratScript.sml and realaxScript.sml actually used the EquivType tool to do quotients; this has now been revised to use the quotient tool. In each case one new well-formedness (respectfulness) theorem had to be proven and included as an argument to the tool. In seqScript.sml, there was a small incompatibility where a definition of a new constant named "-->" conflicted with the constant "--> defined in the quotient library. This was healed by hiding the previous definition before making the new one. All of this was very straightforward. Modified Files: hol98/src/real/hratScript.sml hol98/src/real/hrealScript.sml hol98/src/real/realScript.sml hol98/src/real/realaxScript.sml hol98/src/real/seqScript.sml ----------------------------------------------------------------------
|
#
ecf06adb |
|
20-Jul-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Bad uses of term equalities.
|
#
6cf562f4 |
|
28-Nov-2000 |
Konrad Slind <konrad.slind@gmail.com> |
The reals library builds on Kan.0.
|
#
9f67e582 |
|
10-Jul-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
The function allow_for_overloading_on has been completely removed from the system. The overload code now uses anti-unification of types to figure out the least generalisation of all the types that an overloaded operator needs to represent.
|
#
70493a3d |
|
03-Dec-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix to make it build now that = is non-associative.
|
#
c64241de |
|
01-Dec-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Minor changes to use "jrhUtils" instead of "useful".
|
#
9b4cee77 |
|
22-Sep-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Upgraded to use overloading.
|
#
0058df84 |
|
28-Jun-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixed to bring it up to date with Taupo release 0. (Changes have come across from parse_branch development.)
|
#
58841e67 |
|
29-Apr-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Initial revision
|