document 'case_distrib'
authordesharna
Fri, 19 Dec 2014 11:18:00 +0100
changeset 59268 3f5d6ee7596f
parent 59267 a61257c93d55
child 59269 8713bd81017d
document 'case_distrib'
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]}