equal
deleted
inserted
replaced
9 within that format. This allows to produce papers, books, theses |
9 within that format. This allows to produce papers, books, theses |
10 etc.\ from Isabelle theory sources. |
10 etc.\ from Isabelle theory sources. |
11 |
11 |
12 {\LaTeX} output is generated while processing a \emph{session} in |
12 {\LaTeX} output is generated while processing a \emph{session} in |
13 batch mode, as explained in the \emph{The Isabelle System Manual} |
13 batch mode, as explained in the \emph{The Isabelle System Manual} |
14 \cite{isabelle-sys}. The main Isabelle tools to get started with |
14 @{cite "isabelle-sys"}. The main Isabelle tools to get started with |
15 document preparation are @{tool_ref mkroot} and @{tool_ref build}. |
15 document preparation are @{tool_ref mkroot} and @{tool_ref build}. |
16 |
16 |
17 The classic Isabelle/HOL tutorial \cite{isabelle-hol-book} also |
17 The classic Isabelle/HOL tutorial @{cite "isabelle-hol-book"} also |
18 explains some aspects of theory presentation. *} |
18 explains some aspects of theory presentation. *} |
19 |
19 |
20 |
20 |
21 section {* Markup commands \label{sec:markup} *} |
21 section {* Markup commands \label{sec:markup} *} |
22 |
22 |
421 @{text "proof"} & all proof commands \\ |
421 @{text "proof"} & all proof commands \\ |
422 @{text "ML"} & all commands involving ML code \\ |
422 @{text "ML"} & all commands involving ML code \\ |
423 \end{tabular} |
423 \end{tabular} |
424 |
424 |
425 \medskip The Isabelle document preparation system |
425 \medskip The Isabelle document preparation system |
426 \cite{isabelle-sys} allows tagged command regions to be presented |
426 @{cite "isabelle-sys"} allows tagged command regions to be presented |
427 specifically, e.g.\ to fold proof texts, or drop parts of the text |
427 specifically, e.g.\ to fold proof texts, or drop parts of the text |
428 completely. |
428 completely. |
429 |
429 |
430 For example ``@{command "by"}~@{text "%invisible auto"}'' causes |
430 For example ``@{command "by"}~@{text "%invisible auto"}'' causes |
431 that piece of proof to be treated as @{text invisible} instead of |
431 that piece of proof to be treated as @{text invisible} instead of |
446 by the document author. The Isabelle document preparation tools |
446 by the document author. The Isabelle document preparation tools |
447 also provide some high-level options to specify the meaning of |
447 also provide some high-level options to specify the meaning of |
448 arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding |
448 arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding |
449 parts of the text. Logic sessions may also specify ``document |
449 parts of the text. Logic sessions may also specify ``document |
450 versions'', where given tags are interpreted in some particular way. |
450 versions'', where given tags are interpreted in some particular way. |
451 Again see \cite{isabelle-sys} for further details. |
451 Again see @{cite "isabelle-sys"} for further details. |
452 *} |
452 *} |
453 |
453 |
454 |
454 |
455 section {* Railroad diagrams *} |
455 section {* Railroad diagrams *} |
456 |
456 |