# HG changeset patch
# User blanchet
# Date 1391728742 -3600
# Node ID 6ca9df01ac8c875e22320c7fdb4fd91bb1f87d27
# Parent  12603cbaa844580ce3001469b6f98aba74267e7c
more docs

diff -r 12603cbaa844 -r 6ca9df01ac8c src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Feb 07 00:12:03 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Feb 07 00:19:02 2014 +0100
@@ -1399,14 +1399,14 @@
 text {*
 A datatype selector @{text un_D} can have a default value for each constructor
 on which it is not otherwise specified. Occasionally, it is useful to have the
-default value be defined recursively. This produces a chicken-and-egg situation
-that may seem unsolvable, because the datatype is not introduced yet at the
-moment when the selectors are introduced. Of course, we can always define the
-selectors manually afterward, but we then have to state and prove all the
-characteristic theorems ourselves instead of letting the package do it.
-
-Fortunately, there is a fairly elegant workaround that relies on overloading and
-that avoids the tedium of manual derivations:
+default value be defined recursively. This leads to a chicken-and-egg
+situation, because the datatype is not introduced yet at the moment when the
+selectors are introduced. Of course, we can always define the selectors
+manually afterward, but we then have to state and prove all the characteristic
+theorems ourselves instead of letting the package do it.
+
+Fortunately, there is a workaround that relies on overloading to relieve us
+from the tedium of manual derivations:
 
 \begin{enumerate}
 \setlength{\itemsep}{0pt}
@@ -1452,7 +1452,7 @@
 
 text {* \blankline *}
 
-    lemma terminal_TCons[simp]: "termi (TCons x xs) = termi xs"
+    lemma termi_TCons[simp]: "termi (TCons x xs) = termi xs"
     by (cases xs) auto
 
 
@@ -1613,14 +1613,14 @@
 datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
 iterator and the recursor are replaced by dual concepts:
 
-\begin{itemize}
-\setlength{\itemsep}{0pt}
-
-\item \relax{Coiterator}: @{text unfold_t}
-
-\item \relax{Corecursor}: @{text corec_t}
-
-\end{itemize}
+\medskip
+
+\begin{tabular}{@ {}ll@ {}}
+Coiterator: &
+  @{text unfold_t} \\
+Corecursor: &
+  @{text corec_t}
+\end{tabular}
 *}