# 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