src/Doc/Isar_Ref/Document_Preparation.thy

--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Oct 16 10:11:20 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Oct 16 14:53:26 2015 +0200
@@ -49,8 +49,6 @@
     @@{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
@@ -68,7 +66,6 @@
   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
@@ -187,8 +184,6 @@
   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.
@@ -290,8 +285,6 @@
   @{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>
 
 
@@ -303,8 +296,6 @@
   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.
@@ -318,8 +309,6 @@
   \<^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>
 
 
@@ -329,8 +318,6 @@
   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.
@@ -404,12 +391,12 @@
   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>
@@ -514,8 +501,6 @@
   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>}
@@ -574,8 +559,6 @@
   \<^item> Strict repetition with separator @{verbatim "A + sep"}
 
   @{rail \<open>A + sep\<close>}
-
-  \end{itemize}
 \<close>
 
 
@@ -590,14 +573,10 @@
     @@{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