src/Doc/Isar_Ref/Document_Preparation.thy

   within that format.  This allows to produce papers, books, theses
   etc.\ from Isabelle theory sources.
 
   {\LaTeX} output is generated while processing a \emph{session} in
   batch mode, as explained in the \emph{The Isabelle System Manual}
-  @{cite "isabelle-sys"}.  The main Isabelle tools to get started with
+  @{cite "isabelle-system"}.  The main Isabelle tools to get started with
   document preparation are @{tool_ref mkroot} and @{tool_ref build}.
 
   The classic Isabelle/HOL tutorial @{cite "isabelle-hol-book"} also
   explains some aspects of theory presentation.\<close>
 

     @{text "proof"} & all proof commands \\
     @{text "ML"} & all commands involving ML code \\
   \end{tabular}
 
   \medskip The Isabelle document preparation system
-  @{cite "isabelle-sys"} allows tagged command regions to be presented
+  @{cite "isabelle-system"} allows tagged command regions to be presented
   specifically, e.g.\ to fold proof texts, or drop parts of the text
   completely.
 
   For example ``@{command "by"}~@{text "%invisible auto"}'' causes
   that piece of proof to be treated as @{text invisible} instead of

   by the document author.  The Isabelle document preparation tools
   also provide some high-level options to specify the meaning of
   arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
   parts of the text.  Logic sessions may also specify ``document
   versions'', where given tags are interpreted in some particular way.
-  Again see @{cite "isabelle-sys"} for further details.
+  Again see @{cite "isabelle-system"} for further details.
 \<close>
 
 
 section \<open>Railroad diagrams\<close>