#
179a8c1c |
|
25-Nov-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
New "raw" interface in EmitTeX with user-supplied maps from HOL to LaTeX. The user-supplied maps are consulted first for information about HOL tokens, and if they come up short, the built-in support is used. Given how easy it is to redefine LaTeX commands, this is not likely to be used to override the standard map (choice of variable name in code notwithstanding), but will more likely allow the map to be extended.
|