| changeset 57564 | 4351b7b96abd |
| parent 57558 | 6bb3dd7f8097 |
| child 57575 | b0d31645f47a |
--- a/src/Doc/Datatypes/Datatypes.thy Wed Jul 16 10:13:00 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Jul 16 10:13:38 2014 +0200 @@ -890,6 +890,9 @@ %\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\ %{thm list.rel_cases[no_vars]} +\item[@{text "t."}\hthm{rel_sel}\rm:] ~ \\ +@{thm list.rel_sel[no_vars]} + \end{description} \end{indentblock}