# HG changeset patch
# User blanchet
# Date 1382085357 -7200
# Node ID 97f69d44f73240d8e7d06f3627e5ce43efdee7de
# Parent  297d1c6039993128d003fd324cc7ea20639f4a6f
doc fixes suggested by Andreas L.

diff -r 297d1c603999 -r 97f69d44f732 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Oct 18 10:35:56 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Oct 18 10:35:57 2013 +0200
@@ -806,16 +806,20 @@
 @{thm list.map(1)[no_vars]} \\
 @{thm list.map(2)[no_vars]}
 
-\item[@{text "t."}\hthm{rel\_inject} @{text "[simp, code]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{rel\_inject} @{text "[simp]"}\rm:] ~ \\
 @{thm list.rel_inject(1)[no_vars]} \\
 @{thm list.rel_inject(2)[no_vars]}
 
-\item[@{text "t."}\hthm{rel\_distinct} @{text "[simp, code]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{rel\_distinct} @{text "[simp]"}\rm:] ~ \\
 @{thm list.rel_distinct(1)[no_vars]} \\
 @{thm list.rel_distinct(2)[no_vars]}
 
 \end{description}
 \end{indentblock}
+
+\noindent
+In addition, equational versions of @{text t.rel_inject} and @{text
+rel_distinct} are registered with the @{text "[code]"} attribute.
 *}
 
 
@@ -1403,7 +1407,7 @@
 text {*
 \noindent
 Notice that the @{const cont} selector is associated with both @{const Skip}
-and @{const Choice}.
+and @{const Action}.
 *}
 
 
@@ -2320,8 +2324,9 @@
 suggested major simplifications to the internal constructions, much of which has
 yet to be implemented. Florian Haftmann and Christian Urban provided general
 advice on Isabelle and package writing. Stefan Milius and Lutz Schr\"oder
-found an elegant proof to eliminate one of the BNF assumptions. Christian
-Sternagel suggested many textual improvements to this tutorial.
+found an elegant proof to eliminate one of the BNF assumptions. Andreas
+Lochbihler and Christian Sternagel suggested many textual improvements to this
+tutorial.
 *}
 
 end
diff -r 297d1c603999 -r 97f69d44f732 src/Doc/manual.bib
--- a/src/Doc/manual.bib	Fri Oct 18 10:35:56 2013 +0200
+++ b/src/Doc/manual.bib	Fri Oct 18 10:35:57 2013 +0200
@@ -916,7 +916,7 @@
   note = "\url{https://github.com/frelindb/agsyHOL}"}
 
 @incollection{lochbihler-2010,
-  title = "Coinduction",
+  title = "Coinductive",
   author = "Andreas Lochbihler",
   booktitle = "The Archive of Formal Proofs",
   editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",