1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Dec 02 20:31:54 2013 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Dec 02 20:31:54 2013 +0100
     1.3 @@ -704,8 +704,9 @@
     1.4  (*>*)
     1.5  
     1.6  text {*
     1.7 -The first subgroup of properties is concerned with the constructors.
     1.8 -They are listed below for @{typ "'a list"}:
     1.9 +The free constructor theorems are partitioned in three subgroups. The first
    1.10 +subgroup of properties is concerned with the constructors. They are listed below
    1.11 +for @{typ "'a list"}:
    1.12  
    1.13  \begin{indentblock}
    1.14  \begin{description}
    1.15 @@ -767,7 +768,7 @@
    1.16  \end{indentblock}
    1.17  
    1.18  \noindent
    1.19 -The third and last subgroup revolves around discriminators and selectors:
    1.20 +The third subgroup revolves around discriminators and selectors:
    1.21  
    1.22  \begin{indentblock}
    1.23  \begin{description}
    1.24 @@ -826,7 +827,9 @@
    1.25    \label{sssec:functorial-theorems} *}
    1.26  
    1.27  text {*
    1.28 -The BNF-related theorem are as follows:
    1.29 +The functorial theorems are partitioned in two subgroups. The first subgroup
    1.30 +consists of properties involving the constructors and either a set function, the
    1.31 +map function, or the relator:
    1.32  
    1.33  \begin{indentblock}
    1.34  \begin{description}
    1.35 @@ -853,6 +856,42 @@
    1.36  \noindent
    1.37  In addition, equational versions of @{text t.rel_inject} and @{text
    1.38  rel_distinct} are registered with the @{text "[code]"} attribute.
    1.39 +
    1.40 +The second subgroup consists of more abstract properties of the set functions,
    1.41 +the map function, and the relator:
    1.42 +
    1.43 +\begin{indentblock}
    1.44 +\begin{description}
    1.45 +
    1.46 +\item[@{text "t."}\hthm{map\_comp}\rm:] ~ \\
    1.47 +@{thm list.map_cong0[no_vars]}
    1.48 +
    1.49 +\item[@{text "t."}\hthm{map\_cong} @{text "[cong, fundef_cong]"}\rm:] ~ \\
    1.50 +@{thm list.map_cong[no_vars]}
    1.51 +
    1.52 +\item[@{text "t."}\hthm{map\_id}\rm:] ~ \\
    1.53 +@{thm list.map_id[no_vars]}
    1.54 +
    1.55 +\item[@{text "t."}\hthm{rel\_compp}\rm:] ~ \\
    1.56 +@{thm list.rel_compp[no_vars]}
    1.57 +
    1.58 +\item[@{text "t."}\hthm{rel\_conversep}\rm:] ~ \\
    1.59 +@{thm list.rel_conversep[no_vars]}
    1.60 +
    1.61 +\item[@{text "t."}\hthm{rel\_eq}\rm:] ~ \\
    1.62 +@{thm list.rel_eq[no_vars]}
    1.63 +
    1.64 +\item[@{text "t."}\hthm{rel\_flip}\rm:] ~ \\
    1.65 +@{thm list.rel_flip[no_vars]}
    1.66 +
    1.67 +\item[@{text "t."}\hthm{rel\_mono}\rm:] ~ \\
    1.68 +@{thm list.rel_mono[no_vars]}
    1.69 +
    1.70 +\item[@{text "t."}\hthm{set\_map}\rm:] ~ \\
    1.71 +@{thm list.set_map[no_vars]}
    1.72 +
    1.73 +\end{description}
    1.74 +\end{indentblock}
    1.75  *}
    1.76  
    1.77