equal
deleted
inserted
replaced
219 subsection {* Document preparation \label{sec:document-prep} *} |
219 subsection {* Document preparation \label{sec:document-prep} *} |
220 |
220 |
221 text {* |
221 text {* |
222 Isabelle/Isar provides a simple document preparation system based on |
222 Isabelle/Isar provides a simple document preparation system based on |
223 existing {PDF-\LaTeX} technology, with full support of hyper-links |
223 existing {PDF-\LaTeX} technology, with full support of hyper-links |
224 (both local references and URLs), bookmarks, and thumbnails. Thus |
224 (both local references and URLs) and bookmarks. Thus the results |
225 the results are equally well suited for WWW browsing and as printed |
225 are equally well suited for WWW browsing and as printed copies. |
226 copies. |
226 |
227 |
227 \medskip Isabelle generates {\LaTeX} output as part of the run of a |
228 \medskip |
|
229 |
|
230 Isabelle generates {\LaTeX} output as part of the run of a |
|
231 \emph{logic session} (see also \cite{isabelle-sys}). Getting |
228 \emph{logic session} (see also \cite{isabelle-sys}). Getting |
232 started with a working configuration for common situations is quite |
229 started with a working configuration for common situations is quite |
233 easy by using the Isabelle @{verbatim mkdir} and @{verbatim make} |
230 easy by using the Isabelle @{verbatim mkdir} and @{verbatim make} |
234 tools. First invoke |
231 tools. First invoke |
235 \begin{ttbox} |
232 \begin{ttbox} |