author | desharna |
Mon, 18 Aug 2014 14:09:21 +0200 | |
changeset 57971 | 07e81758788d |
parent 57970 | eaa986cd285a |
child 57980 | 381b3c4fc75a |
--- 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]}