History log of /seL4-l4v-master/HOL4/help/Docfiles/Tactic.UNDISCH_TAC.doc
Revision Date Author Comments
# f969d86b 05-Oct-2017 Andreas Lööw <AndreasLoow@users.noreply.github.com>

Various doc fixes


# d53f48c2 02-Oct-2017 Mario [Castelán Castro] <marioxcc@example.org>

Fix another typographical error in manual entry for “UNDISCH_TAC”.


# 0cd58747 02-Oct-2017 Mario [Castelán Castro] <marioxcc@example.org>

Fix typographical error in manual entry for “UNDISCH_TAC”.


# 6abf0e0c 28-Sep-2017 Mario [Castelán Castro] <marioxcc@example.org>

Fix manual entry of “UNDISCH_TAC”.

Reference: GitHub issue #466
<https://github.com/HOL-Theorem-Prover/HOL/issues/466>.

This contribution (but not future contributions, unless explicitly stated)
is released to the public domain per the CC0 Public Domain Dedication
<https://creativecommons.org/publicdomain/zero/1.0/deed.en>.


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