# HG changeset patch
# User desharna
# Date 1418984280 -3600
# Node ID 3f5d6ee7596f153459ea6d8469dfb808e7b9ead9
# Parent  a61257c93d5550d6384f99e467da2e8552a5117d
document 'case_distrib'

diff -r a61257c93d55 -r 3f5d6ee7596f 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:18:00 2014 +0100
@@ -767,6 +767,9 @@
 \item[@{text "t."}\hthm{case_cong_weak} @{text "[cong]"}\rm:] ~ \\
 @{thm list.case_cong_weak[no_vars]}
 
+\item[@{text "t."}\hthm{case_distrib}\rm:] ~ \\
+@{thm list.case_distrib[no_vars]}
+
 \item[@{text "t."}\hthm{split}\rm:] ~ \\
 @{thm list.split[no_vars]}