<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN">
<HTML>
<HEAD>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=us-ascii">
<META NAME="Generator" CONTENT="MS Exchange Server version 5.5.2657.73">
<TITLE>z_output_theory questions</TITLE>
</HEAD>
<BODY>
<P><FONT SIZE=2>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:</FONT></P>
<P><FONT SIZE=2>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?</FONT></P>
<P><FONT SIZE=2>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.</FONT></P>
<P><FONT SIZE=2>Steve</FONT>
</P>
<P><FONT SIZE=2>Stephen Brackin</FONT>
<BR><FONT SIZE=2>Senior Security Analyst</FONT>
<BR><FONT SIZE=2>CygnaCom Solutions, Inc.</FONT>
<BR><FONT SIZE=2>an Entrust company</FONT>
<BR><FONT SIZE=2>Phone: 607-277-8211 Fax: 607-277-8211</FONT>
<BR><FONT SIZE=2><A HREF="http://www.cygnacom.com" TARGET="_blank">http://www.cygnacom.com</A></FONT>
</P>
<BR>
</BODY>
</HTML>