author | desharna |
Wed, 21 May 2014 18:55:34 +0200 | |
changeset 57047 | 90d4db566e12 |
parent 57046 | b3613d7e108b |
child 57050 | 362c8c64ec83 |
--- a/src/Doc/Datatypes/Datatypes.thy Wed May 21 18:55:34 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed May 21 18:55:34 2014 +0200 @@ -863,6 +863,9 @@ \item[@{text "t."}\hthm{disc\_map\_iff} @{text "[simp]"}\rm:] ~ \\ @{thm list.disc_map_iff[no_vars]} +\item[@{text "t."}\hthm{sel\_map}\rm:] ~ \\ +@{thm list.sel_map[no_vars]} + \item[@{text "t."}\hthm{rel\_inject} @{text "[simp]"}\rm:] ~ \\ @{thm list.rel_inject(1)[no_vars]} \\ @{thm list.rel_inject(2)[no_vars]}