1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed May 25 22:21:38 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 26 13:37:11 2011 +0200
     1.3 @@ -729,14 +729,25 @@
     1.4    HOL.
     1.5  
     1.6    \item \hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}} represents existing types as
     1.7 -  inductive ones, generating the standard infrastructure of derived
     1.8 -  concepts (primitive recursion etc.).
     1.9 +  datatypes.
    1.10 +
    1.11 +  For foundational reasons, some basic types such as \isa{nat}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequote}}}, \isa{bool} and \isa{unit} are
    1.12 +  introduced by more primitive means using \indexref{}{command}{typedef}\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}.  To
    1.13 +  recover the rich infrastructure of \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} (e.g.\ rules
    1.14 +  for \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} and the primitive recursion
    1.15 +  combinators), such types may be represented as actual datatypes
    1.16 +  later.  This is done by specifying the constructors of the desired
    1.17 +  type, and giving a proof of the induction rule, distinctness and
    1.18 +  injectivity of constructors.
    1.19 +
    1.20 +  For example, see \verb|~~/src/HOL/Sum_Type.thy| for the
    1.21 +  representation of the primitive sum type as fully-featured datatype.
    1.22  
    1.23    \end{description}
    1.24  
    1.25 -  The induction and exhaustion theorems generated provide case names
    1.26 -  according to the constructors involved, while parameters are named
    1.27 -  after the types (see also \secref{sec:cases-induct}).
    1.28 +  The generated rules for \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.cases}{\mbox{\isa{cases}}} provide
    1.29 +  case names according to the given constructors, while parameters are
    1.30 +  named after the types (see also \secref{sec:cases-induct}).
    1.31  
    1.32    See \cite{isabelle-HOL} for more details on datatypes, but beware of
    1.33    the old-style theory syntax being used there!  Apart from proper