src/Doc/Datatypes/Datatypes.thy

--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 08 23:09:25 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 08 23:09:34 2014 +0200
@@ -953,8 +953,10 @@
 \item[@{text "t."}\hthm{map_transfer}\rm:] ~ \\
 @{thm list.map_transfer[no_vars]}
 
-\item[@{text "t."}\hthm{rel_compp}\rm:] ~ \\
+\item[@{text "t."}\hthm{rel_compp} @{text "[relator_distr]"}\rm:] ~ \\
 @{thm list.rel_compp[no_vars]}
+(The @{text "[relator_distr]"} attribute is set by the @{text lifting} plugin,
+Section~\ref{ssec:lifting}.)
 
 \item[@{text "t."}\hthm{rel_conversep}\rm:] ~ \\
 @{thm list.rel_conversep[no_vars]}
@@ -969,8 +971,10 @@
 @{thm list.rel_map(1)[no_vars]} \\
 @{thm list.rel_map(2)[no_vars]}
 
-\item[@{text "t."}\hthm{rel_mono}\rm:] ~ \\
+\item[@{text "t."}\hthm{rel_mono} @{text "[relator_mono]"}\rm:] ~ \\
 @{thm list.rel_mono[no_vars]}
+(The @{text "[relator_distr]"} attribute is set by the @{text lifting} plugin,
+Section~\ref{ssec:lifting}.)
 
 \item[@{text "t."}\hthm{rel_transfer}\rm:] ~ \\
 @{thm list.rel_transfer[no_vars]}
@@ -2780,10 +2784,30 @@
   \label{ssec:code-generator} *}
 
 text {*
-The @{text code} plugin registers (co)datatypes for code generation. No
-distinction is made between atatypes and codatatypes. This means that for target
-languages with a strict evaluation strategy (e.g., Standard ML), programs that
-attempt to produce infinite codatatype values will not terminate.
+The @{text code} plugin registers (co)datatypes and other freely generated types
+for code generation. No distinction is made between datatypes and codatatypes.
+This means that for target languages with a strict evaluation strategy (e.g.,
+Standard ML), programs that attempt to produce infinite codatatype values will
+not terminate.
+
+The plugin derives the following properties:
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{eq.refl} @{text "[code nbe]"}\rm:] ~ \\
+@{thm list.eq.refl[no_vars]}
+
+\item[@{text "t."}\hthm{eq.simps} @{text "[code]"}\rm:] ~ \\
+@{thm list.eq.simps(1)[no_vars]} \\
+@{thm list.eq.simps(2)[no_vars]} \\
+@{thm list.eq.simps(3)[no_vars]} \\
+@{thm list.eq.simps(4)[no_vars]} \\
+@{thm list.eq.simps(5)[no_vars]} \\
+@{thm list.eq.simps(6)[no_vars]}
+
+\end{description}
+\end{indentblock}
 *}
 
 
@@ -2825,8 +2849,44 @@
 
 text {*
 For each (co)datatype with live type arguments and each manually registered BNF,
-the @{text transfer} plugin generates properties and attributes that guide the
-Transfer tool.
+the @{text transfer} plugin generates a predicator @{text "t.pred_t"} and
+properties that guide the Transfer tool.
+
+The plugin derives the following properties:
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{Domainp_rel} @{text "[relator_domain]"}\rm:] ~ \\
+@{thm list.Domainp_rel[no_vars]}
+
+\item[@{text "t."}\hthm{pred_inject} @{text "[simp]"}\rm:] ~ \\
+@{thm list.pred_inject(1)[no_vars]} \\
+@{thm list.pred_inject(2)[no_vars]}
+
+\item[@{text "t."}\hthm{rel_eq_onp}\rm:] ~ \\
+@{thm list.rel_eq_onp[no_vars]}
+
+\item[@{text "t."}\hthm{left_total_rel} @{text "[transfer]"}\rm:] ~ \\
+@{thm list.left_total_rel[no_vars]}
+
+\item[@{text "t."}\hthm{left_unique_rel} @{text "[transfer]"}\rm:] ~ \\
+@{thm list.left_unique_rel[no_vars]}
+
+\item[@{text "t."}\hthm{right_total_rel} @{text "[transfer]"}\rm:] ~ \\
+@{thm list.right_total_rel[no_vars]}
+
+\item[@{text "t."}\hthm{right_unique_rel} @{text "[transfer]"}\rm:] ~ \\
+@{thm list.right_unique_rel[no_vars]}
+
+\item[@{text "t."}\hthm{bi_total_rel} @{text "[transfer]"}\rm:] ~ \\
+@{thm list.bi_total_rel[no_vars]}
+
+\item[@{text "t."}\hthm{bi_unique_rel} @{text "[transfer]"}\rm:] ~ \\
+@{thm list.bi_unique_rel[no_vars]}
+
+\end{description}
+\end{indentblock}
 *}
 
 
@@ -2835,7 +2895,24 @@
 
 text {*
 For each (co)datatype with live type arguments and each manually registered BNF,
-the @{text lifting} plugin generates properties that guide the Lifting tool.
+the @{text lifting} plugin generates properties and attributes that guide the
+Lifting tool.
+
+The plugin derives the following property:
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{Quotient} @{text "[quot_map]"}\rm:] ~ \\
+@{thm list.Quotient[no_vars]}
+
+\end{description}
+\end{indentblock}
+
+In addition, the plugins sets the @{text "[relator_eq_onp]"} attribute on a
+variant of the @{text t.rel_eq_onp} property generated by the @{text quotient}
+plugin, the @{text "[relator_mono]"} attribute on @{text t.rel_mono}, and the
+@{text "[relator_distr]"} attribute on @{text t.rel_compp}.
 *}