author | desharna |
Fri, 19 Dec 2014 11:19:14 +0100 | |
changeset 59273 | 2c1e58190664 |
parent 59272 | c6f2867e743f |
child 59274 | 67afe7e6a516 |
--- 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}