# HG changeset patch
# User desharna
# Date 1408367005 -7200
# Node ID d2bc61d7837048a02fbecb056464d7e2dab9a56c
# Parent  81baacfd56e855ef54a0acb29fb6b8c8dbf4beb6
document 'map_cong_simp'

diff -r 81baacfd56e8 -r d2bc61d78370 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 15:03:22 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 15:03:25 2014 +0200
@@ -922,12 +922,15 @@
 \item[@{text "t."}\hthm{set_map}\rm:] ~ \\
 @{thm list.set_map[no_vars]}
 
-\item[@{text "t."}\hthm{map_comp}\rm:] ~ \\
+\item[@{text "t."}\hthm{map_comg0}\rm:] ~ \\
 @{thm list.map_cong0[no_vars]}
 
 \item[@{text "t."}\hthm{map_cong} @{text "[fundef_cong]"}\rm:] ~ \\
 @{thm list.map_cong[no_vars]}
 
+\item[@{text "t."}\hthm{map_cong_simp}\rm:] ~ \\
+@{thm list.map_cong_simp[no_vars]}
+
 \item[@{text "t."}\hthm{map_id}\rm:] ~ \\
 @{thm list.map_id[no_vars]}