History log of /seL4-l4v-master/HOL4/help/Docfiles/Parse.add_rule.doc
Revision Date Author Comments
# e62c6499 04-Oct-2017 Michael Norrish <Michael.Norrish@nicta.com.au>

Remove -- from doc-files.

Thanks to Andreas for pointing this out.


# 754b8318 03-Oct-2014 Piotr Trojanek <piotr.trojanek@gmail.com>

extra space in verbatim text removed


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


# a4c199c6 13-Dec-2001 Michael Norrish <Michael.Norrish@nicta.com.au>

Huge number of check-ins, implementing change to .doc file syntax.
Now the rule for text within braces is that it appears as given, but
that braces must balance. If you want an unbalanced brace, you can use
\lbrace or \rbrace. No existing .doc file uses unbalanced braces.
Also, there is now no need to use \noindent. In fact, doing so
will get you a complaint from the parser. Similarly, use of \ or
{} characters outside of verbatim text blocks will cause griping.
All of the new files have been generated by a parse-then-print process
from the old files, and it's possible there are errors. If you ever
have a spare moment, casting your eye over a random selection of these
might help to find errors.


# ce793cee 23-Nov-2001 Konrad Slind <konrad.slind@gmail.com>

New versions of docfiles.