# Re: [isabelle] Latex without proofs

On Sat, 22 Jun 2013, Holger Blasum wrote:


\paragraph{Printing with usedir, old way}

The old way is:

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



BTW, Isabelle2013 is the last version where the ancient "isabelle usedir" is still there as historical leftover. So starting from the next release, everybody will save a lot of time, by using regular "isabelle build" instead.


At some point I also hope to see document preparation as part of the Prover IDE. Only nostalgy associates latex documents with some batch build job, there are no particular technical reasons (apart from historical legacy getting in the way as usual).



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


In Isabelle/jEdit you can also use the regular "File / Print" operation on text buffers. The output quality is surprisingly high with the default IsabelleText font.


Makarius



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