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