1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Thu Jul 03 11:30:02 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Thu Jul 03 11:30:23 2014 +0200
     1.3 @@ -877,6 +877,10 @@
     1.4  @{thm list.rel_inject(1)[no_vars]} \\
     1.5  @{thm list.rel_inject(2)[no_vars]}
     1.6  
     1.7 +\item[@{text "t."}\hthm{rel\_intros}\rm:] ~ \\
     1.8 +@{thm list.rel_intros(1)[no_vars]} \\
     1.9 +@{thm list.rel_intros(2)[no_vars]}
    1.10 +
    1.11  \item[@{text "t."}\hthm{rel\_distinct} @{text "[simp]"}\rm:] ~ \\
    1.12  @{thm list.rel_distinct(1)[no_vars]} \\
    1.13  @{thm list.rel_distinct(2)[no_vars]}