User Tools
tla:latex
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
tla:latex [2019/09/02 16:58] jonathan |
tla:latex [2019/09/02 17:00] (current) jonathan [More Documentation] |
||
|---|---|---|---|
| Line 58: | Line 58: | ||
| java tla2tex.TeX [options] fileName | java tla2tex.TeX [options] fileName | ||
| - | where [options] is an optional list of options, and fileName is the | + | where [options] is an optional list of options, and ''fileName'' is the |
| - | name of the input file. (If fileName does not contain an extension, | + | name of the input file. (If ''fileName'' does not contain an extension, |
| - | then the input file is fileName.tex.) Running TLATeX with the -help | + | then the input file is ''fileName.tex''.) Running TLATeX with the -help |
| option produces a list of all options. Running it with the -info | option produces a list of all options. Running it with the -info | ||
| option produces what you are now reading. (The fileName can be | option produces what you are now reading. (The fileName can be | ||
| Line 72: | Line 72: | ||
| `pcal' and `ppcal' to `nopcal' or `noppcal' environments. | `pcal' and `ppcal' to `nopcal' or `noppcal' environments. | ||
| - | The only other thing you probably need to know about using tla2tex.TeX | + | Read [[https://lamport.azurewebsites.net/tla/texinfo.txt|here]] for more. |
| - | is how to shade comments, which is explained in the next section. | + | |
tla/latex.1567443517.txt.gz · Last modified: 2019/09/02 16:58 by jonathan
Page Tools
