# HG changeset patch
# User blanchet
# Date 1386012714 -3600
# Node ID 82a78bc9fa0d1d96bf3b351c2e056acacfff405d
# Parent  56fdc6412abc06470213f3ffdbcc65d0b588e358
docs for forgotten BNF theorems

diff -r 56fdc6412abc -r 82a78bc9fa0d src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Dec 02 20:31:54 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Dec 02 20:31:54 2013 +0100
@@ -704,8 +704,9 @@
 (*>*)
 
 text {*
-The first subgroup of properties is concerned with the constructors.
-They are listed below for @{typ "'a list"}:
+The free constructor theorems are partitioned in three subgroups. The first
+subgroup of properties is concerned with the constructors. They are listed below
+for @{typ "'a list"}:
 
 \begin{indentblock}
 \begin{description}
@@ -767,7 +768,7 @@
 \end{indentblock}
 
 \noindent
-The third and last subgroup revolves around discriminators and selectors:
+The third subgroup revolves around discriminators and selectors:
 
 \begin{indentblock}
 \begin{description}
@@ -826,7 +827,9 @@
   \label{sssec:functorial-theorems} *}
 
 text {*
-The BNF-related theorem are as follows:
+The functorial theorems are partitioned in two subgroups. The first subgroup
+consists of properties involving the constructors and either a set function, the
+map function, or the relator:
 
 \begin{indentblock}
 \begin{description}
@@ -853,6 +856,42 @@
 \noindent
 In addition, equational versions of @{text t.rel_inject} and @{text
 rel_distinct} are registered with the @{text "[code]"} attribute.
+
+The second subgroup consists of more abstract properties of the set functions,
+the map function, and the relator:
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{map\_comp}\rm:] ~ \\
+@{thm list.map_cong0[no_vars]}
+
+\item[@{text "t."}\hthm{map\_cong} @{text "[cong, fundef_cong]"}\rm:] ~ \\
+@{thm list.map_cong[no_vars]}
+
+\item[@{text "t."}\hthm{map\_id}\rm:] ~ \\
+@{thm list.map_id[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_compp}\rm:] ~ \\
+@{thm list.rel_compp[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_conversep}\rm:] ~ \\
+@{thm list.rel_conversep[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_eq}\rm:] ~ \\
+@{thm list.rel_eq[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_flip}\rm:] ~ \\
+@{thm list.rel_flip[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_mono}\rm:] ~ \\
+@{thm list.rel_mono[no_vars]}
+
+\item[@{text "t."}\hthm{set\_map}\rm:] ~ \\
+@{thm list.set_map[no_vars]}
+
+\end{description}
+\end{indentblock}
 *}