src/Doc/Isar_Ref/Document_Preparation.thy

       @@{command subsubsection} | @@{command text} | @@{command txt}) @{syntax text}
     ;
     @@{command text_raw} @{syntax text}
   \<close>}
 
-  \begin{description}
-
   \<^descr> @{command chapter}, @{command section}, @{command subsection}, and
   @{command subsubsection} mark chapter and section headings within the
   theory source; this works in any context, even before the initial
   @{command theory} command. The corresponding {\LaTeX} macros are
   @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim \<open>\isamarkupsection\<close>},

   \<^descr> @{command text_raw} inserts {\LaTeX} source directly into the
   output, without additional markup. Thus the full range of document
   manipulations becomes available, at the risk of messing up document
   output.
 
-  \end{description}
 
   Except for @{command "text_raw"}, the text passed to any of the above
   markup commands may refer to formal entities via \emph{document
   antiquotations}, see also \secref{sec:antiq}. These are interpreted in the
   present theory or proof context.

 
   Note that the syntax of antiquotations may \emph{not} include source
   comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
   text @{verbatim "{*"}~@{text "\<dots>"}~@{verbatim "*}"}.
 
-  \begin{description}
-
   \<^descr> @{command "print_antiquotations"} prints all document antiquotations
   that are defined in the current context; the ``@{text "!"}'' option
   indicates extra verbosity.
 
   \<^descr> @{text "@{theory A}"} prints the name @{text "A"}, which is

 
   The {\LaTeX} macro name is determined by the antiquotation option
   @{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 \<open>\nocite{foobar}\<close>}.
-
-  \end{description}
 \<close>
 
 
 subsection \<open>Styled antiquotations\<close>
 

   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:
 
-  \begin{description}
-  
   \<^descr> @{text lhs} extracts the first argument of any application
   form with at least two arguments --- typically meta-level or
   object-level equality, or any other binary relation.
   
   \<^descr> @{text rhs} is like @{text lhs}, but extracts the second

   in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
   
   \<^descr> @{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}
 \<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}
 
   \<^descr> @{antiquotation_option_def show_types}~@{text "= bool"} and
   @{antiquotation_option_def show_sorts}~@{text "= bool"} control
   printing of explicit type and sort constraints.
 

   In contrast, @{antiquotation_option source}~@{text "= true"}
   admits direct printing of the given source text, with the desirable
   well-formedness check in the background, but without modification of
   the printed text.
 
-  \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.\<close>
+  @{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

   Each @{text rule} defines a formal language (with optional name),
   using a notation that is similar to EBNF or regular expressions with
   recursion.  The meaning and visual appearance of these rail language
   elements is illustrated by the following representative examples.
 
-  \begin{itemize}
-
   \<^item> Empty @{verbatim "()"}
 
   @{rail \<open>()\<close>}
 
   \<^item> Nonterminal @{verbatim "A"}

   @{rail \<open>A +\<close>}
 
   \<^item> Strict repetition with separator @{verbatim "A + sep"}
 
   @{rail \<open>A + sep\<close>}
-
-  \end{itemize}
 \<close>
 
 
 section \<open>Draft presentation\<close>
 

 
   @{rail \<open>
     @@{command display_drafts} (@{syntax name} +)
   \<close>}
 
-  \begin{description}
-
   \<^descr> @{command "display_drafts"}~@{text paths} performs simple output of a
   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