# HG changeset patch
# User desharna
# Date 1405498418 -7200
# Node ID 4351b7b96abdb512784b1628009c5c2ef74f6a2c
# Parent  e3e7c86168b4f9fdcb2fd574b61fefba8df8e133
document property 'rel_sel'

diff -r e3e7c86168b4 -r 4351b7b96abd src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Jul 16 10:13:00 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Jul 16 10:13:38 2014 +0200
@@ -890,6 +890,9 @@
 %\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]}
 
+\item[@{text "t."}\hthm{rel_sel}\rm:] ~ \\
+@{thm list.rel_sel[no_vars]}
+
 \end{description}
 \end{indentblock}