1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Tue Oct 19 21:13:10 2010 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Oct 20 20:47:06 2010 +0100
     1.3 @@ -591,12 +591,16 @@
     1.4  
     1.5  text {* Lists are ubiquitous in ML as simple and light-weight
     1.6    ``collections'' for many everyday programming tasks.  Isabelle/ML
     1.7 -  provides some important refinements over the predefined operations
     1.8 -  in SML97. *}
     1.9 +  provides important additions and improvements over operations that
    1.10 +  are predefined in the SML97 library. *}
    1.11  
    1.12  text %mlref {*
    1.13    \begin{mldecls}
    1.14    @{index_ML cons: "'a -> 'a list -> 'a list"} \\
    1.15 +  @{index_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\
    1.16 +  @{index_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
    1.17 +  @{index_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\
    1.18 +  @{index_ML update: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
    1.19    \end{mldecls}
    1.20  
    1.21    \begin{description}
    1.22 @@ -607,11 +611,42 @@
    1.23    The curried @{ML cons} amends this, but it should be only used when
    1.24    partial application is required.
    1.25  
    1.26 +  \item @{ML member}, @{ML insert}, @{ML remove}, @{ML update} treat
    1.27 +  lists as a set-like container that maintains the order of elements.
    1.28 +  See @{"file" "~~/src/Pure/library.ML"} for the full specifications
    1.29 +  (written in ML).  There are some further derived operations like
    1.30 +  @{ML union} or @{ML inter}.
    1.31 +
    1.32 +  Note that @{ML insert} is conservative about elements that are
    1.33 +  already a @{ML member} of the list, while @{ML update} ensures that
    1.34 +  the last entry is always put in front.  The latter discipline is
    1.35 +  often more appropriate in declarations of context data
    1.36 +  (\secref{sec:context-data}) that are issued by the user in Isar
    1.37 +  source: more recent declarations normally take precedence over
    1.38 +  earlier ones.
    1.39 +
    1.40    \end{description}
    1.41  *}
    1.42  
    1.43 +text %mlex {* The following example demonstrates how to \emph{merge}
    1.44 +  two lists in a natural way. *}
    1.45  
    1.46 -subsubsection {* Canonical iteration *}
    1.47 +ML {*
    1.48 +  fun merge_lists eq (xs, ys) = fold_rev (insert eq) ys xs;
    1.49 +*}
    1.50 +
    1.51 +text {* Here the first list is treated conservatively: only the new
    1.52 +  elements from the second list are inserted.  The inside-out order of
    1.53 +  insertion via @{ML fold_rev} attempts to preserve the order of
    1.54 +  elements in the result.
    1.55 +
    1.56 +  This way of merging lists is typical for context data
    1.57 +  (\secref{sec:context-data}).  See also @{ML merge} as defined in
    1.58 +  @{"file" "~~/src/Pure/library.ML"}.
    1.59 +*}
    1.60 +
    1.61 +
    1.62 +subsubsection {* Canonical iteration *}  (* FIXME move!? *)
    1.63  
    1.64  text {* A function @{text "f: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>"} can be understood as update
    1.65    on a configuration of type @{text "\<beta>"} that is parametrized by

     2.1 --- a/doc-src/IsarImplementation/Thy/ML_old.thy	Tue Oct 19 21:13:10 2010 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/ML_old.thy	Wed Oct 20 20:47:06 2010 +0100
     2.3 @@ -319,35 +319,6 @@
     2.4  *}
     2.5  
     2.6  
     2.7 -section {* Common data structures *}
     2.8 -
     2.9 -subsection {* Lists (as set-like data structures) *}
    2.10 -
    2.11 -text {*
    2.12 -  \begin{mldecls}
    2.13 -  @{index_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\
    2.14 -  @{index_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
    2.15 -  @{index_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\
    2.16 -  @{index_ML merge: "('a * 'a -> bool) -> 'a list * 'a list -> 'a list"} \\
    2.17 -  \end{mldecls}
    2.18 -*}
    2.19 -
    2.20 -text {*
    2.21 -  Lists are often used as set-like data structures -- set-like in
    2.22 -  the sense that they support a notion of @{ML member}-ship,
    2.23 -  @{ML insert}-ing and @{ML remove}-ing, but are order-sensitive.
    2.24 -  This is convenient when implementing a history-like mechanism:
    2.25 -  @{ML insert} adds an element \emph{to the front} of a list,
    2.26 -  if not yet present; @{ML remove} removes \emph{all} occurences
    2.27 -  of a particular element.  Correspondingly @{ML merge} implements a 
    2.28 -  a merge on two lists suitable for merges of context data
    2.29 -  (\secref{sec:context-theory}).
    2.30 -
    2.31 -  Functions are parametrized by an explicit equality function
    2.32 -  to accomplish overloaded equality;  in most cases of monomorphic
    2.33 -  equality, writing @{ML "op ="} should suffice.
    2.34 -*}
    2.35 -
    2.36  subsection {* Association lists *}
    2.37  
    2.38  text {*