author | desharna |
Wed, 16 Jul 2014 10:13:38 +0200 | |
changeset 57564 | 4351b7b96abd |
parent 57563 | e3e7c86168b4 |
child 57565 | ab7f39114507 |
--- 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}