# HG changeset patch
# User desharna
# Date 1418984354 -3600
# Node ID 2c1e581906640119851b0ced545da45dfd34112b
# Parent  c6f2867e743f5b139dda8af4a857314f8f0ce259
document 'disc_eq_case'

diff -r c6f2867e743f -r 2c1e58190664 src/Doc/Datatypes/Datatypes.thy
--- 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}