document 'disc_eq_case'

--- a/src/Doc/Datatypes/Datatypes.thy	Mon Jan 05 06:56:15 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Dec 19 11:19:14 2014 +0100
@@ -835,6 +835,10 @@
 \item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\
 @{thm list.case_eq_if[no_vars]}
 
+\item[@{text "t."}\hthm{disc_eq_case}\rm:] ~ \\
+@{thm list.disc_eq_case(1)[no_vars]} \\
+@{thm list.disc_eq_case(2)[no_vars]}
+
 \end{description}
 \end{indentblock}