# HG changeset patch # User traytel # Date 1426543556 -3600 # Node ID 3a1141d56bf1f734a9121a885c4d635471bfe222 # Parent 64c2bb331035db361e8f7ca01e3ecb5d0a9acdb1 document property diff -r 64c2bb331035 -r 3a1141d56bf1 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Mar 16 23:05:56 2015 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Mar 16 23:05:56 2015 +0100 @@ -1001,6 +1001,9 @@ @{thm list.rel_map(1)[no_vars]} \\ @{thm list.rel_map(2)[no_vars]} +\item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\ +@{thm list.rel_refl[no_vars]} + \item[@{text "t."}\hthm{rel_mono} @{text "[mono, relator_mono]"}\rm:] ~ \\ @{thm list.rel_mono[no_vars]} \\ The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin