# HG changeset patch
# User blanchet
# Date 1408382211 -7200
# Node ID 030ff4ceb6c3204c2a9bc28bd69ff034e2dcf2fb
# Parent  ecb227b40907190561616ca24f1f1d8aa185545b
updated docs

diff -r ecb227b40907 -r 030ff4ceb6c3 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 19:16:30 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 19:16:51 2014 +0200
@@ -535,7 +535,7 @@
 variable (@{typ 'a}, @{typ 'b}, \ldots) \cite{isabelle-isar-ref}.
 
 The optional names preceding the type variables allow to override the default
-names of the set functions (@{text set1_t}, \ldots, @{text setM_t}). Type
+names of the set functions (@{text set\<^sub>1_t}, \ldots, @{text set\<^sub>m_t}). Type
 arguments can be marked as dead by entering ``@{text dead}'' in front of the
 type variable (e.g., ``@{text "(dead 'a)"}''); otherwise, they are live or dead
 (and a set function is generated or not) depending on where they occur in the
@@ -647,13 +647,13 @@
 Case combinator: &
   @{text t.case_t} (rendered using the familiar @{text case}--@{text of} syntax) \\
 Discriminators: &
-  @{text "t.is_C\<^sub>1"}$, \ldots, $@{text "t.is_C\<^sub>n"} \\
+  @{text t.is_C\<^sub>1}$, \ldots, $@{text t.is_C\<^sub>n} \\
 Selectors: &
   @{text t.un_C\<^sub>11}$, \ldots, $@{text t.un_C\<^sub>1k\<^sub>1} \\
 & \quad\vdots \\
 & @{text t.un_C\<^sub>n1}$, \ldots, $@{text t.un_C\<^sub>nk\<^sub>n} \\
 Set functions: &
-  @{text t.set1_t}, \ldots, @{text t.setm_t} \\
+  @{text t.set\<^sub>1_t}, \ldots, @{text t.set\<^sub>m_t} \\
 Map function: &
   @{text t.map_t} \\
 Relator: &
@@ -860,7 +860,7 @@
 @{thm list.set(1)[no_vars]} \\
 @{thm list.set(2)[no_vars]}
 
-\item[@{text "t."}\hthm{set_cases}\rm:] ~ \\
+\item[@{text "t."}\hthm{set_cases} @{text "[consumes 1, cases set: set\<^sub>i_t]"}\rm:] ~ \\
 @{thm list.set_cases[no_vars]}
 
 \item[@{text "t."}\hthm{set_empty}\rm:] ~ \\