#
72df737b |
|
25-Feb-2020 |
Magnus Myreen <myreen@chalmers.se> |
Add commands for single quotes
|
#
494e3000 |
|
26-Aug-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Manuals: new LaTeX command for fancy double quotes (instead of ``)
|
#
b69d328b |
|
18-Aug-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update tags to label release as Kananaskis-13
|
#
9f7b0ca2 |
|
13-Aug-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Provide \bq macro for teletype backquote (`) character
|
#
977d64c8 |
|
11-Jun-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Adjust release name in Manuals
|
#
3edf2416 |
|
02-May-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make early Description text more Unicode aware
|
#
e62c6499 |
|
04-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove -- from doc-files. Thanks to Andreas for pointing this out.
|
#
004eebd3 |
|
15-Aug-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Use ##thm command to get nice theorems printed in Description Still many more of these to work through; for the moment only those in the section on finite_mapTheory are done.
|
#
8ef596cc |
|
13-Dec-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More hacking at Description's Tactics chapter
|
#
f9053c22 |
|
08-Oct-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Next release will be Kananaskis-11 This commit starts release preparation branch.
|
#
ef375495 |
|
01-Mar-2015 |
Michael Norrish <michael.norrish@nicta.com.au> |
Set arbitrary traces while LaTeX munging. Closes #141. That issue calls for a slightly different interface to get much the same effect. This approach has the advantage that it keeps the effect of the trace changing localised.
|
#
742e0d6a |
|
05-Nov-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Change Kananaskis-9 into Kananaskis-10 in the relevant places.
|
#
a30a20b7 |
|
28-Oct-2014 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make \ie, \eg and \etc LaTeX macros expand to text in italic shape.
|
#
a5cea6d8 |
|
17-Aug-2014 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
DESCRIPTION: fixed punctuation, style and typography of 'etc.'
|
#
a67f15de |
|
01-Aug-2014 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
Typography: problematic macros marked with FIXME notes.
|
#
299c76d4 |
|
01-Dec-2013 |
Michael Norrish <michael.norrish@nicta.com.au> |
Updated version number in manuals, banners etc.
|
#
a49170b6 |
|
24-Jul-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Change HOL macro in manuals to be \textsc{Hol}. The old macro was to {{\small HOL}} which meant that uses of \HOL in things like section titles looked awful. The new form looks better in that context but may well not be the final word.
|
#
53a23ba6 |
|
17-Aug-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update version numbers now that K7 is out.
|
#
f8d4f895 |
|
08-Sep-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Bump version numbers - next release to be 'Kananaskis-7'.
|
#
58f9662f |
|
29-Jul-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
From now on we're in the Brave New World of Kananaskis 6.
|
#
004bea20 |
|
31-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add some documentation of the "syntactic patterns" feature.
|
#
530b7722 |
|
28-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Write a brief section on Unicode features in the parser.
|
#
2f0017e3 |
|
04-Feb-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Much hacking about with the Description manual. Section headings more consistent, index tidied, some prose written about tokens in the brave new world of Unicode aware parsing.
|
#
53fa769c |
|
29-Apr-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Have "modernised" the manuals. 1. By default it now uses pdflatex. Postscript can still be generated with "make ps". * Authors should not use pstricks - it doesn't work with pdflatex. * The commuting diagrams in the tutorial have been redone with XP-pic -- with much less code. * Other figures can be included with "\includegraphics", which is provided by the graphicx package. Just make sure you upload EPS and PDF versions of the diagrams. * The Covers directory and old logos have been removed -- they weren't maintainable. (Have tarted up the title.tex pages.) 2. The make files have been updated and cleaned up. There is now "make clean" option in $HOLDIR/Manuals. * As a side note, I noticed that a call to "make" in $HOLDIR/Manuals didn't do anything on Mac OS X. I had to do "make -B". 3. Have eliminated font substitution errors. * Don't include the charter.sty package - the font is now changed in LaTeX/layout.sty. This avoids changing the \tt font, which causes problems with \section{\texttt{stuff}}. * Left and right braces in \tt font can be a problem. \{ and \} give maths font, which is fine in places. \verb%{}% will work but \verb can't be used in certain places (inside another command). Have added \lb and \rb to LaTeX/commands.tex. These are just \char'173 and \char'175 and can be used anywhere. 4. Have commented out the mucking about with page numbering. * This means that if you do a goto page N (in Acrobat, Preview.app etc.) then you go to page N of the main text. (Stops folks having to add an offset to entries in the index.) 5. Have made things more compatible with amsmath. * The environment "boxed" (LaTeX/commands.tex) has been renamed to "holboxed". * Have changed "\over" to "\frac". * amsmath is turned on in the Logic manual, mainly to get text subscripts typesetting better. 6. Have removed a bunch of hbox (and other) warnings. * Don't do "\begin{session}\begin{hol}\begin{verbatim}...", do "\begin{session}\begin{verbatim}..." instead. * Don't use "\begin{hol}\begin{verbatim}..." is item lists. Instead just do "\begin{verbatim}". * Have done some small text edits - hopefully these are okay. * A few more warnings remain and there's not much that can be done about underfull vboxes -- short of going with "\raggedbottom". 7. Have made Doc2TeX and reference.tex used fancyvrb, This means the font size can be set to \small globally. Have also removed the \samepage directive -- a few bad breaks are better than having material bigger than the size of the page.
|
#
97f5eef8 |
|
02-Jan-2007 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Bump our release number to 5, for the next release. Will probably remove the original uses in help/src and just make these reference the Globals module.
|
#
25eec758 |
|
06-Oct-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
New command for the fourth manual.
|
#
5eacf25c |
|
29-Sep-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Another place where version numbers get bumped for the next release.
|
#
4e276e1e |
|
13-Jul-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Minor index hacks, as well as adjusting the \holquote macro to print out a more accurate reflection of what the user sees (\tt backquotes, in other words).
|
#
e2eeb1c7 |
|
03-Feb-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add new \holtxt command. Intention is to ultimately replace all those ugly \verb+..+ and {\small\verb+...+} with calls to \holtxt and \ml, depending on the nature of the contents. Currently, both \holtxt and \ml look the same, but distinguishing is still worthwhile I think. To get backslashes in \holtxt or \ml, use \bs.
|
#
75052611 |
|
17-Dec-2004 |
Konrad Slind <konrad.slind@gmail.com> |
Added a macro or two.
|
#
7248bcee |
|
23-Sep-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Some useful commands, including one for generating a texttt backslash, that's \bs.
|
#
23e0fc2e |
|
07-Mar-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update the numbers corresponding to our version number.
|
#
e632700c |
|
06-Jul-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update holversion macros for new release and remove unused VERSION macro.
|
#
55982dcb |
|
30-Sep-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Modified Holmake to support a -i (or --interactive) command-line flag. (This is feature request #611879.) Modified documentation to reflect this and slightly updated some other things in the Description that caught my eye.
|
#
27d999f0 |
|
21-Aug-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove annoying messages about \sl not being allowed in math-mode by replacing occurrences with \textsl. Also remove unused files hol98.dot and hol98.pic.
|
#
cf2bf05a |
|
22-Apr-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Most important hol98 purging action.
|
#
56a589c3 |
|
12-Apr-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changed the session environment so that they can be \label-ed, and then later \ref-ed.
|
#
f52b808c |
|
15-Jan-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Updated macro for release name and version number.
|
#
ee181486 |
|
26-Oct-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Updated version number to 5.
|
#
374877dc |
|
10-Jul-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Modified so that the hol version number information is accessed through a macro, defined in the LaTeX/commands.tex file. This allows it to be changed in one place instead of many.
|
#
54d461a6 |
|
16-Dec-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
\holn macro now defined in commands.tex.
|
#
f46471c6 |
|
25-Aug-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Removed the \see command, which is defined by the makeidx package.
|
#
6fc6e5ae |
|
04-Aug-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Useful parts of the hol88 directory; copied across for hol98 and some slightly updated.
|