src/Doc/Isar_Ref/Outer_Syntax.thy

 
   @{rail \<open>
     @@{command help} (@{syntax name} * )
   \<close>}
 
-  \begin{description}
-
   \<^descr> @{command "print_commands"} prints all outer syntax keywords
   and commands.
 
   \<^descr> @{command "help"}~@{text "pats"} retrieves outer syntax
   commands according to the specified name patterns.
-
-  \end{description}
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 

 section \<open>Lexical matters \label{sec:outer-lex}\<close>
 
 text \<open>The outer lexical syntax consists of three main categories of
   syntax tokens:
 
-  \begin{enumerate}
-
   \<^enum> \emph{major keywords} --- the command names that are available
   in the present logic session;
 
   \<^enum> \emph{minor keywords} --- additional literal tokens required
   by the syntax of commands;
 
   \<^enum> \emph{named tokens} --- various categories of identifiers etc.
 
-  \end{enumerate}
 
   Major keywords and minor keywords are guaranteed to be disjoint.
   This helps user-interfaces to determine the overall structure of a
   theory text, without knowing the full details of command syntax.
   Internally, there is some additional information about the kind of

   existing theorems.  Existing theorems are given by @{syntax thmref}
   and @{syntax thmrefs}, the former requires an actual singleton
   result.
 
   There are three forms of theorem references:
-  \begin{enumerate}
 
   \<^enum> named facts @{text "a"},
 
   \<^enum> selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
 
   \<^enum> literal fact propositions using token syntax @{syntax_ref altstring}
   @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} or @{syntax_ref cartouche}
   @{text "\<open>\<phi>\<close>"} (see also method @{method_ref fact}).
 
-  \end{enumerate}
 
   Any kind of theorem specification may include lists of attributes
   both on the left and right hand sides; attributes are applied to any
   immediately preceding fact.  If names are omitted, the theorems are
   not stored within the theorem database of the theory or proof

 
   These commands print certain parts of the theory and proof context.
   Note that there are some further ones available, such as for the set
   of rules declared for simplifications.
 
-  \begin{description}
-
   \<^descr> @{command "print_theory"} prints the main logical content of the
   background theory; the ``@{text "!"}'' option indicates extra verbosity.
 
   \<^descr> @{command "print_definitions"} prints dependencies of definitional
   specifications within the background theory, which may be constants

   or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and
   that are never used.
   If @{text n} is @{text 0}, the end of the range of theories
   defaults to the current theory. If no range is specified,
   only the unused theorems in the current theory are displayed.
-
-  \end{description}
 \<close>
 
 end