Re: [isabelle] Latex without proofs

Dear Stephan,

On 06-21, Stephan van Staden wrote:
> Is there a simple way to suppress all proofs when presenting
> theories with Isabelle/Latex?

Yes. Use option document_variants="document:outline=/proof".

FWIW (there may be better ways), inlined an excerpt from my working 

\subsection{PDF generation}

\paragraph{Proper PDF generation nowadays}

The new way is to have file called ``ROOT'':

session "test" = "HOL" +
  options [document = pdf, document_output = "output", document_variants="document:outline=/proof", quick_and_dirty=true]
  theories [document = false]
    (* Foo Bar *)
  files "document/root.tex"

Then invoke:

$ isabelle build -D .


\item ``document\_output'' forces generation of output into directory output (must exist)
\item ``outline=/proof'' forces generation of an {\em additional} file called ``outline.pdf'' which is not containing proofs, documented in Isabelle documentation system.pdf, Section ``Isabelle Sessions and Build Management'', ``System build options'' (in particular see p. 21 in Isabelle 2013 version of system.pdf) 
\item ``quick\_and\_dirty=true'': allows sorry
\item ``document/root.tex'' see below (old way)

\paragraph{Printing with usedir, old way}

The old way is:

$ isabelle usedir -d pdf  HOL .

needs document/root.tex with
\parindent 0pt\parskip 0.5ex

and ROOT.ML with 
quick_and_dirty := true;
use_thy "test";

Note that this automatically adds included theories to the document.
If quick\_and\_dirty is omitted only theories without cheating (``sorry'') 
are accepted.

\paragraph{Quick scratch notes}

>From Proof General, do ``Isabelle $\rightarrow$ Commands $\rightarrow$ display draft''.

>From Isabelle/jedit use the Isar command display\_drafts ``file-name''. From Isabelle/Eclipse, I have not figured out how to use display\_drafts, but print\_drafts (sending to default printer) can be used.

display\_drafts and print\_drafts is documented in isar-ref.pdf, ``Document preparation'', ``Draft presentation''.

\paragraph{Printable comments}

Printable comments can be specified as follows:

text {* *}
--"this is a comment"

The second version can be used within proof steps.
Within \{* text *\} blocks, underscores need to be escaped once.
When ``--'' is used, underscores need to be escaped twice.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.