| changeset 57933 | f620851148a9 |
| parent 57894 | 6c992a4bcfbd |
| child 57969 | 1e7b9579b14f |
--- a/src/Doc/Datatypes/Datatypes.thy Thu Aug 14 13:20:54 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Aug 14 13:21:19 2014 +0200 @@ -943,6 +943,10 @@ \item[@{text "t."}\hthm{rel_flip}\rm:] ~ \\ @{thm list.rel_flip[no_vars]} +\item[@{text "t."}\hthm{rel_map}\rm:] ~ \\ +@{thm list.rel_map(1)[no_vars]} \\ +@{thm list.rel_map(2)[no_vars]} + \item[@{text "t."}\hthm{rel_mono}\rm:] ~ \\ @{thm list.rel_mono[no_vars]}