document property
authortraytel
Mon Mar 16 23:05:56 2015 +0100 (2015-03-16)
changeset 597273a1141d56bf1
parent 59726 64c2bb331035
child 59729 ba54b27d733d
document property
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Mar 16 23:05:56 2015 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Mar 16 23:05:56 2015 +0100
     1.3 @@ -1001,6 +1001,9 @@
     1.4  @{thm list.rel_map(1)[no_vars]} \\
     1.5  @{thm list.rel_map(2)[no_vars]}
     1.6  
     1.7 +\item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\
     1.8 +@{thm list.rel_refl[no_vars]}
     1.9 +
    1.10  \item[@{text "t."}\hthm{rel_mono} @{text "[mono, relator_mono]"}\rm:] ~ \\
    1.11  @{thm list.rel_mono[no_vars]} \\
    1.12  The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin