diff -r 151f894984d8 -r 2bf52eec4e8a src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Oct 14 15:06:42 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Oct 14 15:10:32 2015 +0200
@@ -49,10 +49,10 @@
 
   \begin{description}
 
-  \item @{command "print_commands"} prints all outer syntax keywords
+  \<^descr> @{command "print_commands"} prints all outer syntax keywords
   and commands.
 
-  \item @{command "help"}~@{text "pats"} retrieves outer syntax
+  \<^descr> @{command "help"}~@{text "pats"} retrieves outer syntax
   commands according to the specified name patterns.
 
   \end{description}
@@ -505,35 +505,35 @@
 
   \begin{description}
 
-  \item @{command "print_theory"} prints the main logical content of the
+  \<^descr> @{command "print_theory"} prints the main logical content of the
   background theory; the ``@{text "!"}'' option indicates extra verbosity.
 
-  \item @{command "print_definitions"} prints dependencies of definitional
+  \<^descr> @{command "print_definitions"} prints dependencies of definitional
   specifications within the background theory, which may be constants
   \secref{sec:consts} or types (\secref{sec:types-pure},
   \secref{sec:hol-typedef}); the ``@{text "!"}'' option indicates extra
   verbosity.
 
-  \item @{command "print_methods"} prints all proof methods available in the
+  \<^descr> @{command "print_methods"} prints all proof methods available in the
   current theory context; the ``@{text "!"}'' option indicates extra
   verbosity.
 
-  \item @{command "print_attributes"} prints all attributes available in the
+  \<^descr> @{command "print_attributes"} prints all attributes available in the
   current theory context; the ``@{text "!"}'' option indicates extra
   verbosity.
 
-  \item @{command "print_theorems"} prints theorems of the background theory
+  \<^descr> @{command "print_theorems"} prints theorems of the background theory
   resulting from the last command; the ``@{text "!"}'' option indicates
   extra verbosity.
 
-  \item @{command "print_facts"} prints all local facts of the current
+  \<^descr> @{command "print_facts"} prints all local facts of the current
   context, both named and unnamed ones; the ``@{text "!"}'' option indicates
   extra verbosity.
 
-  \item @{command "print_term_bindings"} prints all term bindings that
+  \<^descr> @{command "print_term_bindings"} prints all term bindings that
   are present in the context.
 
-  \item @{command "find_theorems"}~@{text criteria} retrieves facts
+  \<^descr> @{command "find_theorems"}~@{text criteria} retrieves facts
   from the theory or proof context matching all of given search
   criteria.  The criterion @{text "name: p"} selects all theorems
   whose fully qualified name matches pattern @{text p}, which may
@@ -555,7 +555,7 @@
   default, duplicates are removed from the search result. Use
   @{text with_dups} to display duplicates.
 
-  \item @{command "find_consts"}~@{text criteria} prints all constants
+  \<^descr> @{command "find_consts"}~@{text criteria} prints all constants
   whose type meets all of the given criteria. The criterion @{text
   "strict: ty"} is met by any type that matches the type pattern
   @{text ty}.  Patterns may contain both the dummy type ``@{text _}''
@@ -564,11 +564,11 @@
   the prefix ``@{text "-"}'' function as described for @{command
   "find_theorems"}.
 
-  \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
+  \<^descr> @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
   visualizes dependencies of facts, using Isabelle's graph browser
   tool (see also @{cite "isabelle-system"}).
 
-  \item @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"}
+  \<^descr> @{command "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"}
   displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}
   or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and
   that are never used.