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 
cheatsheet:

\subsection{PDF generation}

\paragraph{Proper PDF generation nowadays}

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

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

Then invoke:

\begin{lstlisting}
$ isabelle build -D .
\end{lstlisting}

Explanation:

\begin{itemize} 
\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)
\end{itemize}

\paragraph{Printing with usedir, old way}

The old way is:

\begin{lstlisting}
$ isabelle usedir -d pdf  HOL .
\end{lstlisting}

needs document/root.tex with
\begin{lstlisting}
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}
\urlstyle{rm}
\isabellestyle{it}
\begin{document}
\title{}
\author{}
\maketitle
\tableofcontents
\parindent 0pt\parskip 0.5ex
\input{session}
\end{document}
\end{lstlisting}

and ROOT.ML with 
\begin{lstlisting}
quick_and_dirty := true;
use_thy "test";
\end{lstlisting}

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:

\begin{lstlisting}
text {* *}
--"this is a comment"
\end{lstlisting}

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.

best,

-- 
Holger




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