1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed May 25 22:21:38 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 26 13:37:11 2011 +0200
     1.3 @@ -458,14 +458,26 @@
     1.4    HOL.
     1.5  
     1.6    \item @{command (HOL) "rep_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 @{typ nat}, @{typ
    1.12 +  "'a \<times> 'b"}, @{typ "'a + 'b"}, @{typ bool} and @{typ unit} are
    1.13 +  introduced by more primitive means using @{command_ref typedef}.  To
    1.14 +  recover the rich infrastructure of @{command datatype} (e.g.\ rules
    1.15 +  for @{method cases} and @{method induct} and the primitive recursion
    1.16 +  combinators), such types may be represented as actual datatypes
    1.17 +  later.  This is done by specifying the constructors of the desired
    1.18 +  type, and giving a proof of the induction rule, distinctness and
    1.19 +  injectivity of constructors.
    1.20 +
    1.21 +  For example, see @{file "~~/src/HOL/Sum_Type.thy"} for the
    1.22 +  representation of the primitive sum type as fully-featured datatype.
    1.23  
    1.24    \end{description}
    1.25  
    1.26 -  The induction and exhaustion theorems generated provide case names
    1.27 -  according to the constructors involved, while parameters are named
    1.28 -  after the types (see also \secref{sec:cases-induct}).
    1.29 +  The generated rules for @{method induct} and @{method cases} provide
    1.30 +  case names according to the given constructors, while parameters are
    1.31 +  named after the types (see also \secref{sec:cases-induct}).
    1.32  
    1.33    See \cite{isabelle-HOL} for more details on datatypes, but beware of
    1.34    the old-style theory syntax being used there!  Apart from proper