[ProofPower] z_output_theory questions

[Stephen Brackin]

I'm trying to produce a nice printout of the theory I'm working in for
future reference, but have run into a couple of questions:

1. Why does z_output_theory produce only a fragment of a document, not a
full document that docdvi can process without error?  I was able to work
around this by patching standard LaTeX beginning and ending lines into the
document, but why should this be necessary?

2. Is there any way to get z_output_theory to produce a listing that doesn't
show the types of all constants?  I have a fairly small theory, but with all
the type information its listing is over 100 pages long.

Steve

Stephen Brackin
Senior Security Analyst
CygnaCom Solutions, Inc.
an Entrust company
Phone: 607-277-8211 Fax:  607-277-8211
http://www.cygnacom.com


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040910/5534d999/attachment.htm>