| changeset 57969 | 1e7b9579b14f |
| parent 57933 | f620851148a9 |
| child 57971 | 07e81758788d |
--- a/src/Doc/Datatypes/Datatypes.thy Mon Aug 18 13:46:26 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Aug 18 13:49:47 2014 +0200 @@ -913,6 +913,9 @@ \begin{indentblock} \begin{description} +\item[@{text "t."}\hthm{inj_map}\rm:] ~ \\ +@{thm list.inj_map[no_vars]} + \item[@{text "t."}\hthm{set_map}\rm:] ~ \\ @{thm list.set_map[no_vars]}