# HG changeset patch
# User blanchet
# Date 1379523452 -7200
# Node ID 0c565fec9c78a57f15b0af2fcca8daaf0b531c17
# Parent  9b034e6b977ce26ce82822708d1c8b0a32af87c1
updated docs

diff -r 9b034e6b977c -r 0c565fec9c78 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Sep 18 18:57:09 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Sep 18 18:57:32 2013 +0200
@@ -754,6 +754,10 @@
 @{thm list.disc(1)[no_vars]} \\
 @{thm list.disc(2)[no_vars]}
 
+\item[@{text "t."}\hthm{discI}\rm:] ~ \\
+@{thm list.discI(1)[no_vars]} \\
+@{thm list.discI(2)[no_vars]}
+
 \item[@{text "t."}\hthm{sel} @{text "[simp]"}\rm:] ~ \\
 @{thm list.sel(1)[no_vars]} \\
 @{thm list.sel(2)[no_vars]}
@@ -1512,11 +1516,11 @@
 @{thm llist.corec(1)[no_vars]} \\
 @{thm llist.corec(2)[no_vars]}
 
-\item[@{text "t."}\hthm{disc\_unfold} @{text "[simp]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{disc\_unfold}\rm:] ~ \\
 @{thm llist.disc_unfold(1)[no_vars]} \\
 @{thm llist.disc_unfold(2)[no_vars]}
 
-\item[@{text "t."}\hthm{disc\_corec} @{text "[simp]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{disc\_corec}\rm:] ~ \\
 @{thm llist.disc_corec(1)[no_vars]} \\
 @{thm llist.disc_corec(2)[no_vars]}