src/Doc/Datatypes/Datatypes.thy
changeset 57982 d2bc61d78370
parent 57971 07e81758788d
child 57983 6edc3529bb4e
     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