diff -r 08f465e23dc5 -r 909e00299009 doc-src/Logics/Old_HOL.tex
--- a/doc-src/Logics/Old_HOL.tex	Thu Aug 25 12:21:00 1994 +0200
+++ b/doc-src/Logics/Old_HOL.tex	Wed Aug 31 17:34:12 1994 +0200
@@ -1247,10 +1247,10 @@
 
 A datatype declaration has the following general structure:
 \[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~
-      c_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~
-      c_m(\tau_{m1},\dots,\tau_{mk_m}) 
+      C_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~
+      C_m(\tau_{m1},\dots,\tau_{mk_m}) 
 \]
-where $\alpha_i$ are type variables, $c_i$ are distinct constructor names and
+where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and
 $\tau_{ij}$ are one of the following:
 \begin{itemize}
 \item type variables $\alpha_1,\dots,\alpha_n$,
@@ -1262,17 +1262,24 @@
     least one constructor must consist of only non-recursive type
     components.}
 \end{itemize}
+If you would like one of the $\tau_{ij}$ to be a complex type expression
+$\tau$ you need to declare a new type synonym $syn = \tau$ first and use
+$syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the
+recursive type itself, thus ruling out problematic cases like \[ \mbox{\tt
+  datatype}~ t ~=~ C(t \To t) \] together with unproblematic ones like \[
+\mbox{\tt datatype}~ t ~=~ C(t~list). \]
+
 The constructors are automatically defined as functions of their respective
 type:
-\[ c_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \]
+\[ C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \]
 These functions have certain {\em freeness} properties:
 \begin{description}
 \item[\tt distinct] They are distinct:
-\[ c_i(x_1,\dots,x_{k_i}) \neq c_j(y_1,\dots,y_{k_j}) \qquad
+\[ C_i(x_1,\dots,x_{k_i}) \neq C_j(y_1,\dots,y_{k_j}) \qquad
    \mbox{for all}~ i \neq j.
 \]
 \item[\tt inject] They are injective:
-\[ (c_j(x_1,\dots,x_{k_j}) = c_j(y_1,\dots,y_{k_j})) =
+\[ (C_j(x_1,\dots,x_{k_j}) = C_j(y_1,\dots,y_{k_j})) =
    (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j})
 \]
 \end{description}
@@ -1282,9 +1289,9 @@
 natural number
 \[
 \begin{array}{lcl}
-\mbox{\it t\_ord}(c_1(x_1,\dots,x_{k_1})) & = & 0 \\
+\mbox{\it t\_ord}(C_1(x_1,\dots,x_{k_1})) & = & 0 \\
 & \vdots & \\
-\mbox{\it t\_ord}(c_m(x_1,\dots,x_{k_m})) & = & m-1
+\mbox{\it t\_ord}(C_m(x_1,\dots,x_{k_m})) & = & m-1
 \end{array}
 \]
 and distinctness of constructors is expressed by:
@@ -1297,11 +1304,11 @@
 {\begin{array}{lcl}
 \Forall x_1\dots x_{k_1}.
   \List{P(x_{r_{11}}); \dots; P(x_{r_{1l_1}})} &
-  \Imp  & P(c_1(x_1,\dots,x_{k_1})) \\
+  \Imp  & P(C_1(x_1,\dots,x_{k_1})) \\
  & \vdots & \\
 \Forall x_1\dots x_{k_m}.
   \List{P(x_{r_{m1}}); \dots; P(x_{r_{ml_m}})} &
-  \Imp & P(c_m(x_1,\dots,x_{k_m}))
+  \Imp & P(C_m(x_1,\dots,x_{k_m}))
 \end{array}}
 \]
 where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji}
@@ -1311,9 +1318,9 @@
 The type also comes with an \ML-like \sdx{case}-construct:
 \[
 \begin{array}{rrcl}
-\mbox{\tt case}~e~\mbox{\tt of} & c_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\
+\mbox{\tt case}~e~\mbox{\tt of} & C_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\
                            \vdots \\
-                           \mid & c_m(x_{m1},\dots,x_{mk_m}) & \To & e_m
+                           \mid & C_m(x_{m1},\dots,x_{mk_m}) & \To & e_m
 \end{array}
 \]
 In contrast to \ML, {\em all} constructors must be present, their order is
@@ -1553,7 +1560,7 @@
 \item[HOL/ex/InSort.ML] and {\tt HOL/ex/Qsort.ML} contain correctness
   proofs about insertion sort and quick sort.
 
-\item[HOL/ex/PL.ML] proves the soundness and completeness of classical
+\item[HOL/ex/PropLog.ML] proves the soundness and completeness of classical
   propositional logic, given a truth table semantics.  The only connective
   is $\imp$.  A Hilbert-style axiom system is specified, and its set of
   theorems defined inductively.  A similar proof in \ZF{} is described