# HG changeset patch
# User desharna
# Date 1404742006 -7200
# Node ID 7027cf5c1f2ccdd06d11d845e33264c0af1d6f91
# Parent  f9dd8a33f82045ae553ee73fbbae90f7feee64ce
document property 'rel_cases'

diff -r f9dd8a33f820 -r 7027cf5c1f2c src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Jul 07 16:06:46 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Jul 07 16:06:46 2014 +0200
@@ -877,13 +877,16 @@
 @{thm list.rel_inject(1)[no_vars]} \\
 @{thm list.rel_inject(2)[no_vars]}
 
+\item[@{text "t."}\hthm{rel\_distinct} @{text "[simp]"}\rm:] ~ \\
+@{thm list.rel_distinct(1)[no_vars]} \\
+@{thm list.rel_distinct(2)[no_vars]}
+
 \item[@{text "t."}\hthm{rel\_intros}\rm:] ~ \\
 @{thm list.rel_intros(1)[no_vars]} \\
 @{thm list.rel_intros(2)[no_vars]}
 
-\item[@{text "t."}\hthm{rel\_distinct} @{text "[simp]"}\rm:] ~ \\
-@{thm list.rel_distinct(1)[no_vars]} \\
-@{thm list.rel_distinct(2)[no_vars]}
+\item[@{text "t."}\hthm{rel\_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\
+@{thm list.rel_cases[no_vars]}
 
 \end{description}
 \end{indentblock}