updated docs
authorblanchet
Mon Aug 18 19:16:51 2014 +0200 (2014-08-18)
changeset 57988030ff4ceb6c3
parent 57987 ecb227b40907
child 57989 45873fcbbf2e
updated docs
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 19:16:30 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 19:16:51 2014 +0200
     1.3 @@ -535,7 +535,7 @@
     1.4  variable (@{typ 'a}, @{typ 'b}, \ldots) \cite{isabelle-isar-ref}.
     1.5  
     1.6  The optional names preceding the type variables allow to override the default
     1.7 -names of the set functions (@{text set1_t}, \ldots, @{text setM_t}). Type
     1.8 +names of the set functions (@{text set\<^sub>1_t}, \ldots, @{text set\<^sub>m_t}). Type
     1.9  arguments can be marked as dead by entering ``@{text dead}'' in front of the
    1.10  type variable (e.g., ``@{text "(dead 'a)"}''); otherwise, they are live or dead
    1.11  (and a set function is generated or not) depending on where they occur in the
    1.12 @@ -647,13 +647,13 @@
    1.13  Case combinator: &
    1.14    @{text t.case_t} (rendered using the familiar @{text case}--@{text of} syntax) \\
    1.15  Discriminators: &
    1.16 -  @{text "t.is_C\<^sub>1"}$, \ldots, $@{text "t.is_C\<^sub>n"} \\
    1.17 +  @{text t.is_C\<^sub>1}$, \ldots, $@{text t.is_C\<^sub>n} \\
    1.18  Selectors: &
    1.19    @{text t.un_C\<^sub>11}$, \ldots, $@{text t.un_C\<^sub>1k\<^sub>1} \\
    1.20  & \quad\vdots \\
    1.21  & @{text t.un_C\<^sub>n1}$, \ldots, $@{text t.un_C\<^sub>nk\<^sub>n} \\
    1.22  Set functions: &
    1.23 -  @{text t.set1_t}, \ldots, @{text t.setm_t} \\
    1.24 +  @{text t.set\<^sub>1_t}, \ldots, @{text t.set\<^sub>m_t} \\
    1.25  Map function: &
    1.26    @{text t.map_t} \\
    1.27  Relator: &
    1.28 @@ -860,7 +860,7 @@
    1.29  @{thm list.set(1)[no_vars]} \\
    1.30  @{thm list.set(2)[no_vars]}
    1.31  
    1.32 -\item[@{text "t."}\hthm{set_cases}\rm:] ~ \\
    1.33 +\item[@{text "t."}\hthm{set_cases} @{text "[consumes 1, cases set: set\<^sub>i_t]"}\rm:] ~ \\
    1.34  @{thm list.set_cases[no_vars]}
    1.35  
    1.36  \item[@{text "t."}\hthm{set_empty}\rm:] ~ \\