# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID 67e9fdd9ae9e937cdd0c3384cf0dbacf0b528109
# Parent  c2506f61fd267113bbf0039739bf9d70fb458e1a
updated docs

diff -r c2506f61fd26 -r 67e9fdd9ae9e src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -771,7 +771,7 @@
 @{thm list.case(1)[no_vars]} \\
 @{thm list.case(2)[no_vars]}
 
-\item[@{text "t."}\hthm{case\_cong}\rm:] ~ \\
+\item[@{text "t."}\hthm{case\_cong} @{text "[fundef_cong]"}\rm:] ~ \\
 @{thm list.case_cong[no_vars]}
 
 \item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}\rm:] ~ \\
@@ -2605,6 +2605,9 @@
 
 \noindent
 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
+For technical reasons, the @{text "[fundef_cong]"} attribute is not set on the
+generated @{text case_cong} theorem. It can be added manually using
+\keyw{declare}.
 *}