proof obligations, proofs into LateX/LaTeX2e, including a viewing and
printing tool. Documents may be customized through the `Options'
palette to automatically include cross references at the clause and
construct level, and a full index including all variables, constants,
sets, operations and machines. Each AMN construct may be freely
annotated (not just commented) each annotation being faithfully
reproduced in the final document.