#
42536ae7 |
|
14-Mar-2018 |
Andreas Lööw <AndreasLoow@users.noreply.github.com> |
Fix rendering of ligatures for words theory The package stix enables T1 font encoding, which affects how e.g. >> and -- are rendered in monospace fonts. This fix disables this (using the microtype package). This fix also moves the stix package to the common style file, so all documentation is formatted consistently.
|
#
79dce081 |
|
23-Aug-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Remove redundant index and tableofcontents commands from Manual LaTeX files.
|
#
7c534cd2 |
|
27-May-2009 |
Peter Homeier <palantir@trustworthytools.com> |
Fixes an unintended change made in revision 6812.
|
#
06b4cee6 |
|
27-May-2009 |
Peter Homeier <palantir@trustworthytools.com> |
In preparation for making the standard kernel build under Poly/ML, removed the dependency of src/0/Term.sml on the Moscow ML library Polyhash, replacing this with RedBlackMap. The building of HOL appears to be faster with RedBlackMap. Also revised RedBlackMap.sml, RedBlackSet.sml, and HolKernel.sml to eliminate some annoying warning messages.
|
#
af9314b7 |
|
29-Apr-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Use the standard LaTeX bibliography but keep the "References" heading.
|
#
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.
|
#
6f66085b |
|
29-Jul-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Copied across from HOL88; slight changes to make it LateX2e compatible.
|