doc-src/HOL/HOL.tex

 which associates to the right and has a lower priority than $*$: $\tau@1 +
 \tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.
 
 The definition of products and sums in terms of existing types is not
 shown.  The constructions are fairly standard and can be found in the
-respective theory files.
+respective theory files. Although the sum and product types are
+constructed manually for foundational reasons, they are represented as
+actual datatypes later (see \S\ref{subsec:datatype:rep_datatype}).
+Therefore, the theory \texttt{Datatype} should be used instead of
+\texttt{Sum} or \texttt{Prod}.
 
 \begin{figure}
 \begin{constants}
   \it symbol    & \it meta-type &           & \it description \\ 
   \cdx{Inl}     & $\alpha \To \alpha+\beta$    & & first injection\\
   \cdx{Inr}     & $\beta \To \alpha+\beta$     & & second injection\\
   \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
         & & conditional
 \end{constants}
 \begin{ttbox}\makeatletter
-%\tdx{sum_case_def}   sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) &
-%                                        (!y. p=Inr y --> z=g y))
-%
 \tdx{Inl_not_Inr}    Inl a ~= Inr b
 
 \tdx{inj_Inl}        inj Inl
 \tdx{inj_Inr}        inj Inr
 

 
 \tdx{sum_case_Inl}   sum_case f g (Inl x) = f x
 \tdx{sum_case_Inr}   sum_case f g (Inr x) = g x
 
 \tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
-\tdx{split_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
+\tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
                                      (! y. s = Inr(y) --> R(g(y))))
 \end{ttbox}
 \caption{Type $\alpha+\beta$}\label{hol-sum}
 \end{figure}
 

 case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\)
 \end{ttbox}
 Note that Isabelle insists on precisely this format; you may not even change
 the order of the two cases.
 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
-\cdx{nat_rec}, the details of which can be found in theory \texttt{NatDef}.
+\cdx{nat_rec}, which is available because \textit{nat} is represented as
+a datatype (see \S\ref{subsec:datatype:rep_datatype}).
 
 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
 %Recursion along this relation resembles primitive recursion, but is
 %stronger because we are in higher-order logic; using primitive recursion to
 %define a higher-order function, we can easily Ackermann's function, which

   distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}.
 In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct}
 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
 
 
-\subsection{Representing existing types as datatypes}
+\subsection{Representing existing types as datatypes}\label{subsec:datatype:rep_datatype}
 
 For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt
   +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,
 but by more primitive means using \texttt{typedef}. To be able to use the
 tactics \texttt{induct_tac} and \texttt{exhaust_tac} and to define functions by