| changeset 57971 | 07e81758788d |
| parent 57969 | 1e7b9579b14f |
| child 57982 | d2bc61d78370 |
--- a/src/Doc/Datatypes/Datatypes.thy Mon Aug 18 14:09:09 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Aug 18 14:09:21 2014 +0200 @@ -916,6 +916,9 @@ \item[@{text "t."}\hthm{inj_map}\rm:] ~ \\ @{thm list.inj_map[no_vars]} +\item[@{text "t."}\hthm{inj_map_strong}\rm:] ~ \\ +@{thm list.inj_map_strong[no_vars]} + \item[@{text "t."}\hthm{set_map}\rm:] ~ \\ @{thm list.set_map[no_vars]}