#
e62c6499 |
|
04-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove -- from doc-files. Thanks to Andreas for pointing this out.
|
#
8f6d7784 |
|
16-Nov-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Delete trailing whitespace in help/Docfiles
|
#
d92257e5 |
|
31-Oct-2014 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
Prim_rec: whitespace cleanup in both .sig and .doc
|
#
3825a653 |
|
10-Aug-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Purge on broken links within the (HTML) documentation. This mostly involves deleting SEEALSO entries (where documentation doesn't exist) but also fixing a few links. Also fixed the anchor links in TheoryIndex.html and idIndex.html. In both cases there aren't any entries starting with the letter "Y".
|
#
83b175a9 |
|
20-Sep-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed a bunch of rarely used functions from hol88Lib. Related documentation updated. The ancient hol88 interface should disappear eventually; code using it should be properly ported to use the current HOL functions instead.
|
#
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.
|
#
9b49e9da |
|
06-Dec-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Many fixups, most to do with braces not being doubled properly in a slew of .doc files. Also, remember to provide an identifier after the initial \DOC.
|
#
ce793cee |
|
23-Nov-2001 |
Konrad Slind <konrad.slind@gmail.com> |
New versions of docfiles.
|