[ProofPower] z_output_theory questions

[Roger Bishop Jones]

On Friday 10 September 2004  5:04 am, Stephen Brackin wrote:

> 1. Why does z_output_theory produce only a fragment of a
> document, not a full document that docdvi can process without
> error?

So that the theory listing can be included in some other
document, e.g. the document containing the material
which created the theory.

> I was able to work around this by patching standard
> LaTeX beginning and ending lines into the document, but why
> should this be necessary?

Its easier to add top and tail than to remove them if you
don't want them.

> 2. Is there any way to get z_output_theory to produce a
> listing that doesn't show the types of all constants?

I don't think so.

> I have a fairly small theory, but with all the type
> information its listing is over 100 pages long.

You could probably prepare a custom sieve steering file to
solve both of your problems, i.e. to automatically add the
head and tail you require and to discard any sections
you don't want.

Look in section 6 of the document preparation manual (USR001).
Use sieve with your own steering file instead of doctex,
and then use texdvi.
Make a custom steering file by editing the standard one
(which is $PPINSTALLDIR/etc/sieveview).

Alternatively (and probably faster) write a perl script
to process the theory listing.

Roger Jones