src/Doc/Datatypes/Datatypes.thy
changeset 75276 686a6d7d0991
parent 74666 432b3605933d
child 75624 22d1c5f2b9f4
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Mar 11 09:23:05 2022 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Mar 11 11:19:38 2022 +0100
@@ -982,6 +982,9 @@
 \item[\<open>t.\<close>\hthm{map_ident}\rm:] ~ \\
 @{thm list.map_ident[no_vars]}
 
+\item[\<open>t.\<close>\hthm{map_ident_strong}\rm:] ~ \\
+@{thm list.map_ident_strong[no_vars]}
+
 \item[\<open>t.\<close>\hthm{map_transfer} \<open>[transfer_rule]\<close>\rm:] ~ \\
 @{thm list.map_transfer[no_vars]} \\
 The \<open>[transfer_rule]\<close> attribute is set by the \<open>transfer\<close> plugin