# HG changeset patch
# User blanchet
# Date 1391728323 -3600
# Node ID 12603cbaa844580ce3001469b6f98aba74267e7c
# Parent  1d2852dfc4a7a123500f3b3e3f66e6532c82242d
docs

diff -r 1d2852dfc4a7 -r 12603cbaa844 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Feb 06 23:09:22 2014 +0000
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Feb 07 00:12:03 2014 +0100
@@ -378,7 +378,7 @@
 
 text {*
 \noindent
-The introduced constants are listed below.
+The types of the constants that appear in the specification are listed below.
 
 \medskip
 
@@ -646,32 +646,30 @@
 @{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the
 following auxiliary constants are introduced:
 
-\begin{itemize}
-\setlength{\itemsep}{0pt}
-
-\item \relax{Case combinator}: @{text t.case_t} (rendered using the familiar
-@{text case}--@{text of} syntax)
-
-\item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,
-@{text "t.is_C\<^sub>n"}
-
-\item \relax{Selectors}:
-@{text t.un_C\<^sub>11}$, \ldots, @{text t.un_C\<^sub>1k\<^sub>1}, \\
-\phantom{\relax{Selectors:}} \quad\vdots \\
-\phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.
-
-\item \relax{Set functions} (or \relax{natural transformations}):
-@{text set1_t}, \ldots, @{text t.setm_t}
-
-\item \relax{Map function} (or \relax{functorial action}): @{text t.map_t}
-
-\item \relax{Relator}: @{text t.rel_t}
-
-\item \relax{Iterator}: @{text t.fold_t}
-
-\item \relax{Recursor}: @{text t.rec_t}
-
-\end{itemize}
+\medskip
+
+\begin{tabular}{@ {}ll@ {}}
+Case combinator: &
+  @{text t.case_t} (rendered using the familiar @{text case}--@{text of} syntax) \\
+Discriminators: &
+  @{text "t.is_C\<^sub>1"}$, \ldots, $@{text "t.is_C\<^sub>n"} \\
+Selectors: &
+  @{text t.un_C\<^sub>11}$, \ldots, $@{text t.un_C\<^sub>1k\<^sub>1} \\
+& \quad\vdots \\
+& @{text t.un_C\<^sub>n1}$, \ldots, $@{text t.un_C\<^sub>nk\<^sub>n} \\
+Set functions: &
+  @{text set1_t}, \ldots, @{text t.setm_t} \\
+Map function: &
+  @{text t.map_t} \\
+Relator: &
+  @{text t.rel_t} \\
+Iterator: &
+   @{text t.fold_t} \\
+Recursor: &
+  @{text t.rec_t}
+\end{tabular}
+
+\medskip
 
 \noindent
 The case combinator, discriminators, and selectors are collectively called