document 'map_cong_simp'
authordesharna
Mon Aug 18 15:03:25 2014 +0200 (2014-08-18)
changeset 57982d2bc61d78370
parent 57981 81baacfd56e8
child 57983 6edc3529bb4e
child 58001 934d85f14d1d
document 'map_cong_simp'
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 15:03:22 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 15:03:25 2014 +0200
     1.3 @@ -922,12 +922,15 @@
     1.4  \item[@{text "t."}\hthm{set_map}\rm:] ~ \\
     1.5  @{thm list.set_map[no_vars]}
     1.6  
     1.7 -\item[@{text "t."}\hthm{map_comp}\rm:] ~ \\
     1.8 +\item[@{text "t."}\hthm{map_comg0}\rm:] ~ \\
     1.9  @{thm list.map_cong0[no_vars]}
    1.10  
    1.11  \item[@{text "t."}\hthm{map_cong} @{text "[fundef_cong]"}\rm:] ~ \\
    1.12  @{thm list.map_cong[no_vars]}
    1.13  
    1.14 +\item[@{text "t."}\hthm{map_cong_simp}\rm:] ~ \\
    1.15 +@{thm list.map_cong_simp[no_vars]}
    1.16 +
    1.17  \item[@{text "t."}\hthm{map_id}\rm:] ~ \\
    1.18  @{thm list.map_id[no_vars]}
    1.19