# HG changeset patch
# User desharna
# Date 1408363761 -7200
# Node ID 07e81758788d6edb4ead1cbbcf7a069169b6b795
# Parent  eaa986cd285a8189c48def9722ad59853bbaa3c8
document 'inj_map_strong'

diff -r eaa986cd285a -r 07e81758788d src/Doc/Datatypes/Datatypes.thy
--- 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]}