src/Doc/Isar_Ref/Document_Preparation.thy

 theory Document_Preparation
 imports Base Main
 begin
 
-chapter {* Document preparation \label{ch:document-prep} *}
-
-text {* Isabelle/Isar provides a simple document preparation system
+chapter \<open>Document preparation \label{ch:document-prep}\<close>
+
+text \<open>Isabelle/Isar provides a simple document preparation system
   based on {PDF-\LaTeX}, with support for hyperlinks and bookmarks
   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
   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.  *}
-
-
-section {* Markup commands \label{sec:markup} *}
-
-text {*
+  explains some aspects of theory presentation.\<close>
+
+
+section \<open>Markup commands \label{sec:markup}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "header"} & : & @{text "toplevel \<rightarrow> toplevel"} \\[0.5ex]
     @{command_def "chapter"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "section"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "subsection"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

 
   \medskip The proof markup commands closely resemble those for theory
   specifications, but have a different formal status and produce
   different {\LaTeX} macros.  The default definitions coincide for
   analogous commands such as @{command section} and @{command sect}.
-*}
-
-
-section {* Document Antiquotations \label{sec:antiq} *}
-
-text {*
+\<close>
+
+
+section \<open>Document Antiquotations \label{sec:antiq}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{antiquotation_def "theory"} & : & @{text antiquotation} \\
     @{antiquotation_def "thm"} & : & @{text antiquotation} \\
     @{antiquotation_def "lemma"} & : & @{text antiquotation} \\
     @{antiquotation_def "prop"} & : & @{text antiquotation} \\

   @{antiquotation_option_def cite_macro}, or the configuration option
   @{attribute cite_macro} in the context. For example, @{text "@{cite
   [cite_macro = nocite] foobar}"} produces @{verbatim "\\nocite{foobar}"}.
 
   \end{description}
-*}
-
-
-subsection {* Styled antiquotations *}
-
-text {* The antiquotations @{text thm}, @{text prop} and @{text
+\<close>
+
+
+subsection \<open>Styled antiquotations\<close>
+
+text \<open>The antiquotations @{text thm}, @{text prop} and @{text
   term} admit an extra \emph{style} specification to modify the
   printed result.  A style is specified by a name with a possibly
   empty number of arguments;  multiple styles can be sequenced with
   commas.  The following standard styles are available:
 

   \item @{text "prem"} @{text n} extract premise number
   @{text "n"} from from a rule in Horn-clause
   normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
 
   \end{description}
-*}
-
-
-subsection {* General options *}
-
-text {* The following options are available to tune the printed output
+\<close>
+
+
+subsection \<open>General options\<close>
+
+text \<open>The following options are available to tune the printed output
   of antiquotations.  Note that many of these coincide with system and
   configuration options of the same names.
 
   \begin{description}
 

   \end{description}
 
   For Boolean flags, ``@{text "name = true"}'' may be abbreviated as
   ``@{text name}''.  All of the above flags are disabled by default,
   unless changed specifically for a logic session in the corresponding
-  @{verbatim "ROOT"} file.  *}
-
-
-section {* Markup via command tags \label{sec:tags} *}
-
-text {* Each Isabelle/Isar command may be decorated by additional
+  @{verbatim "ROOT"} file.\<close>
+
+
+section \<open>Markup via command tags \label{sec:tags}\<close>
+
+text \<open>Each Isabelle/Isar command may be decorated by additional
   presentation tags, to indicate some modification in the way it is
   printed in the document.
 
   @{rail \<open>
     @{syntax_def tags}: ( tag * )

   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.
-*}
-
-
-section {* Railroad diagrams *}
-
-text {*
+\<close>
+
+
+section \<open>Railroad diagrams\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{antiquotation_def "rail"} & : & @{text antiquotation} \\
   \end{matharray}
 
   @{rail \<open>

   \item Strict repetition with separator @{verbatim "A + sep"}
 
   @{rail \<open>A + sep\<close>}
 
   \end{itemize}
-*}
-
-
-section {* Draft presentation *}
-
-text {*
+\<close>
+
+
+section \<open>Draft presentation\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
   \end{matharray}
 
   @{rail \<open>

   given list of raw source files. Only those symbols that do not require
   additional {\LaTeX} packages are displayed properly, everything else is left
   verbatim.
 
   \end{description}
-*}
+\<close>
 
 end