document property 'rel_map'
authordesharna
Thu Aug 14 13:21:19 2014 +0200 (2014-08-14)
changeset 57933f620851148a9
parent 57932 c29659f77f8d
child 57943 52c68f8126a8
document property 'rel_map'
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Thu Aug 14 13:20:54 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Thu Aug 14 13:21:19 2014 +0200
     1.3 @@ -943,6 +943,10 @@
     1.4  \item[@{text "t."}\hthm{rel_flip}\rm:] ~ \\
     1.5  @{thm list.rel_flip[no_vars]}
     1.6  
     1.7 +\item[@{text "t."}\hthm{rel_map}\rm:] ~ \\
     1.8 +@{thm list.rel_map(1)[no_vars]} \\
     1.9 +@{thm list.rel_map(2)[no_vars]}
    1.10 +
    1.11  \item[@{text "t."}\hthm{rel_mono}\rm:] ~ \\
    1.12  @{thm list.rel_mono[no_vars]}
    1.13