Useful LaTeX Packages

by Leslie Lamport

Last modified 7 October 2011

Each package listed here is documented by comments at the beginning of its file. To read the comments, open the file in any text editor or word processor using a fixed-width font. The pf2 package also has a separate document describing how to use it. While I've tried to document all their idiosynchrasies, the tla2 and abbrev styles are not as robust as the standard styles. Use them at your own risk.

pf2.sty: 7 September 2011
This package is for writing the kinds of structured proofs introduced in How to Write a Proof and the forthcoming How to Write a 21st Century Proof. It has genuine documentation. See also the pfnum program.
tla2.sty: 18 November 1998
Helps in writing TLA (Temporal Logic of Actions) formulas and proofs, and TLA+ specifications. It defines commands and environments for TLA+ modules, and also defines abbreviations that I find useful in math mode, such as [] for \Box and => for \Rightarrow . The comments include instructions for how you can modify the package to produce the abbreviations that you will find useful. The package loads the pf2.sty and abbrev.sty packages.
abbrev.sty: 4 September 1994
Allows you to define your own abbreviations--for example to define (+) to be equivalent to \ensuremath{\oplus} .

Obsolete Style Files

The following are obsolete, but they are here in case anyone encounters a source file for a document that uses them.

tla.sty: 18 November 1998
Helps in writing TLA (Temporal Logic of Actions) formulas and proofs, and TLA+ specifications. Defines commands and environments for TLA+ modules, and useful abbreviations, such as [] for \Box and => for \Rightarrow . It loads pf.sty (described below) and abbrev.sty (described above).
pf.sty: 19 January 1998
Defines commands and environments for writing formulas and structured proofs.
spec92.sty: 29 October 1995
This is a LaTeX-2.09 document-style option, but it should also work as a LaTeX-2e packages It defines a spec environment for printing an ASCII specification. The environment is like verbatim, except that \ works as usual, and various abbreviations are defined--for example, [] for \Box and => for \Rightarrow .

This page can be found by searching the Web for the 23-letter string uidlamportlatexpackages. Please do not put this string in any document that could wind up on the web--including email messages and pdf and Word documents. You can refer to it in Web documents as "the string obtained by removing the - from uid-lamportlatexpackages".