#
ba8a2281 |
|
01-Dec-2017 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Added TeX notation for relation inversion (relinv)
|
#
c50549af |
|
19-Oct-2017 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Added TeX_notation for "++" in listTheory
|
#
6ac7f1da |
|
02-Aug-2017 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Added TeX notation for O (relation composition)
|
#
6eaae01a |
|
15-Jul-2017 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
TeX notations for RUNION, RINTER and RSUBSET in relationTheory
|
#
d2d3cc44 |
|
02-Nov-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Pretty-printer now annotates consts with their real names and types. In "complicated" overload situations, such as the overloads for NOTIN and <>, the annotation can't point to a "real" underlying constant, but does still provide the type for the emacs tool-tips. In passing, also create a new annotation form, the SymConst as well as the Const. This is done for the TeX backend's benefit, so that it can avoid treating things like + the same as normal identifiers. This works well for math-mode munging where you want "+" to map to $+$, but want "INSERT" to map to \textsf{INSERT}. Closes #39
|
#
ed9860cf |
|
29-Oct-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Finish documenting math-mode munging. Closes #121.
|
#
a83e2652 |
|
29-Sep-2014 |
Ramana Kumar <ramana@member.fsf.org> |
translate tildes in EmitTeX strings Made an new HOLTokenTilde command as the target. The default behaviour of that command might be improved, but I don't know how (typesetting a tilde nicely in TeX is apparently pretty hard...).
|
#
0f4aa1d1 |
|
24-Aug-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Handle character literals when printing to LaTeX Closes #190. See also 89b5d3224403 for first piece of work in this vein.
|
#
5a3337e2 |
|
13-Aug-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Define \HOLFieldName macro rather than \HOLFldName Bug spotted by Ramana.
|
#
89b5d322 |
|
27-Jul-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Create new PP backend annotations for literals (strings, numbers, ...) Use these to emit string literals via a \HOLStringLit macro that can be redefined to get better output than my default. Of course, it's quite possible that my \textrm{``#1''} is not even a reasonable default. Note how the HOLStringLit macro is given an argument that doesn't have the quotation mark delimiters around it.
|
#
c5e63297 |
|
17-Jun-2014 |
Ramana Kumar <ramana@member.fsf.org> |
add rulename option to LaTeX munger for naming inference rules Allows the user to provide a string (name) to be passed as the optional argument to \infer[name]{...} when typesetting using rule or stackedrule. Due to the simplistic parsing of the munger's commands and options, unexpected results are likely if this name contains any special characters. (Perhaps it should parse them under some encoding for this option?) The name is wrapped in a new \HOLRuleName command, which provides a route for customisation.
|
#
bd4bf27a |
|
18-Jan-2013 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Provide for special typesetting of type-operators in EmitTeX. This uses back-end annotations.
|
#
4b8cb0e3 |
|
15-Jan-2013 |
Michael Norrish <michael.norrish@nicta.com.au> |
Use Const annotations in the TeX pretty-printing backend. Intention is to allow users to redefine \HOLConst to set their constant names in something other than the default \texttt.
|
#
ee07838a |
|
04-Feb-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make EmitTeX always use a tt double-quote (around strings).
|
#
1a2269a1 |
|
20-Jul-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Give isPREFIX symbols TeX equivalents.
|
#
ea493c8e |
|
10-May-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Allow empty list forms to be overloaded ([], {}, etc). This gives us the ability to get nice TeX for them. Instantiate this ability for emptyset.
|
#
732573f3 |
|
06-May-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Merging \inlineHOL in holindex.sty with Michael's newly added \HOLinline in holtexbasic.sty. To keep things consistent "blockHOL" has been renamed to "HOLblock" and moved to holtexbasic.sty.
|
#
3efaef51 |
|
05-May-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Provide another level of indirection for HOL inline stuff. New LaTeX command, \HOLinline{....}.
|
#
d8c7abd2 |
|
04-May-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
First attempt at TeX notation for lazy list brackets.
|
#
d728bf39 |
|
04-May-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add TeX notation for 'proper subset'.
|
#
2f9c806c |
|
04-May-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add TeX notation for bag delimiters.
|
#
9deb2c8d |
|
22-Apr-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix leaching of boldness from HOLKeyword command by adding braces.
|
#
4e32bd26 |
|
21-Apr-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add TeX notations for some HOL keywords: if-then-else, case-of, let-and-in and do-od.
|
#
355b8c3a |
|
10-Apr-2010 |
Ramana Kumar <ramana.kumar@gmail.com> |
Added HOLTokenDot to holtexbasic.sty
|
#
c1db6473 |
|
15-Mar-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Give a TeX binding for Hilbert choice, now generated in TeX from @.
|
#
cdde6ba5 |
|
21-Jan-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add support for super- and sub-scripts in the LaTeX backend of EmitTeX.
|
#
e45dbe94 |
|
21-Jan-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix errors in last EmitTeX check-in. Handle superscript -1 in overrides.
|
#
91ae3118 |
|
16-Jan-2010 |
Ramana Kumar <ramana.kumar@gmail.com> |
More unicode symbols for EmitTeX's string_map. Also added new HOLTokens for rhd, left and right small triangles, and composition (circ).
|
#
bd5375aa |
|
13-Jan-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More symbols for EmitTeX (subset and submap).
|
#
c2044a74 |
|
25-Nov-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Use annotation information to italicise variables in EmitTeX. This can be customised through LaTeX redefinition of the commands \HOLFreeVar and \HOLBoundVar. Both current make their arguments \mathit.
|
#
541c454e |
|
25-Nov-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add union and intersection to EmitTeX's known symbols.
|
#
15787973 |
|
10-Nov-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add superscript star and plus to EmitTeX. Generalisation opportunities probably exist.
|
#
aa33d490 |
|
29-Oct-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Added new (Unicode) symbols to EmitTeX
|
#
1e6626b6 |
|
22-Oct-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
holtexbasic.sty: \notin looks slightly better than \not\in.
|
#
8ff5fc86 |
|
21-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improve printing of HOL data types -- now more compact. Extended the filtering to eliminate big record definitions. Added LaTeX tokens for IN (\in) and NOTIN (\not\in).
|
#
ddf12293 |
|
01-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update to EmitTeX, following changes to pretty-printing in HOL.
|
#
58a5e6f6 |
|
03-Jul-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a leftarrow token.
|
#
fb8e53b3 |
|
06-Mar-2009 |
Konrad Slind <konrad.slind@gmail.com> |
Moving TeX.
|