| changeset 59268 | 3f5d6ee7596f |
| parent 58935 | dcad9bad43e7 |
| child 59273 | 2c1e58190664 |
--- 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]}