1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 18 18:57:09 2013 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Sep 18 18:57:32 2013 +0200
     1.3 @@ -754,6 +754,10 @@
     1.4  @{thm list.disc(1)[no_vars]} \\
     1.5  @{thm list.disc(2)[no_vars]}
     1.6  
     1.7 +\item[@{text "t."}\hthm{discI}\rm:] ~ \\
     1.8 +@{thm list.discI(1)[no_vars]} \\
     1.9 +@{thm list.discI(2)[no_vars]}
    1.10 +
    1.11  \item[@{text "t."}\hthm{sel} @{text "[simp]"}\rm:] ~ \\
    1.12  @{thm list.sel(1)[no_vars]} \\
    1.13  @{thm list.sel(2)[no_vars]}
    1.14 @@ -1512,11 +1516,11 @@
    1.15  @{thm llist.corec(1)[no_vars]} \\
    1.16  @{thm llist.corec(2)[no_vars]}
    1.17  
    1.18 -\item[@{text "t."}\hthm{disc\_unfold} @{text "[simp]"}\rm:] ~ \\
    1.19 +\item[@{text "t."}\hthm{disc\_unfold}\rm:] ~ \\
    1.20  @{thm llist.disc_unfold(1)[no_vars]} \\
    1.21  @{thm llist.disc_unfold(2)[no_vars]}
    1.22  
    1.23 -\item[@{text "t."}\hthm{disc\_corec} @{text "[simp]"}\rm:] ~ \\
    1.24 +\item[@{text "t."}\hthm{disc\_corec}\rm:] ~ \\
    1.25  @{thm llist.disc_corec(1)[no_vars]} \\
    1.26  @{thm llist.disc_corec(2)[no_vars]}
    1.27