# HG changeset patch
# User wenzelm
# Date 1287604026 -3600
# Node ID bbac63bbcffe0a2d6dfaf11f55c5944feaf8d6ba
# Parent  b70cd46e8e4488747e56cfe6c5ed7fdde108560d
clarified "lists as a set-like container";

diff -r b70cd46e8e44 -r bbac63bbcffe doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Tue Oct 19 21:13:10 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Oct 20 20:47:06 2010 +0100
@@ -591,12 +591,16 @@
 
 text {* Lists are ubiquitous in ML as simple and light-weight
   ``collections'' for many everyday programming tasks.  Isabelle/ML
-  provides some important refinements over the predefined operations
-  in SML97. *}
+  provides important additions and improvements over operations that
+  are predefined in the SML97 library. *}
 
 text %mlref {*
   \begin{mldecls}
   @{index_ML cons: "'a -> 'a list -> 'a list"} \\
+  @{index_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\
+  @{index_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
+  @{index_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\
+  @{index_ML update: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
   \end{mldecls}
 
   \begin{description}
@@ -607,11 +611,42 @@
   The curried @{ML cons} amends this, but it should be only used when
   partial application is required.
 
+  \item @{ML member}, @{ML insert}, @{ML remove}, @{ML update} treat
+  lists as a set-like container that maintains the order of elements.
+  See @{"file" "~~/src/Pure/library.ML"} for the full specifications
+  (written in ML).  There are some further derived operations like
+  @{ML union} or @{ML inter}.
+
+  Note that @{ML insert} is conservative about elements that are
+  already a @{ML member} of the list, while @{ML update} ensures that
+  the last entry is always put in front.  The latter discipline is
+  often more appropriate in declarations of context data
+  (\secref{sec:context-data}) that are issued by the user in Isar
+  source: more recent declarations normally take precedence over
+  earlier ones.
+
   \end{description}
 *}
 
+text %mlex {* The following example demonstrates how to \emph{merge}
+  two lists in a natural way. *}
 
-subsubsection {* Canonical iteration *}
+ML {*
+  fun merge_lists eq (xs, ys) = fold_rev (insert eq) ys xs;
+*}
+
+text {* Here the first list is treated conservatively: only the new
+  elements from the second list are inserted.  The inside-out order of
+  insertion via @{ML fold_rev} attempts to preserve the order of
+  elements in the result.
+
+  This way of merging lists is typical for context data
+  (\secref{sec:context-data}).  See also @{ML merge} as defined in
+  @{"file" "~~/src/Pure/library.ML"}.
+*}
+
+
+subsubsection {* Canonical iteration *}  (* FIXME move!? *)
 
 text {* A function @{text "f: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>"} can be understood as update
   on a configuration of type @{text "\<beta>"} that is parametrized by
diff -r b70cd46e8e44 -r bbac63bbcffe doc-src/IsarImplementation/Thy/ML_old.thy
--- a/doc-src/IsarImplementation/Thy/ML_old.thy	Tue Oct 19 21:13:10 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML_old.thy	Wed Oct 20 20:47:06 2010 +0100
@@ -319,35 +319,6 @@
 *}
 
 
-section {* Common data structures *}
-
-subsection {* Lists (as set-like data structures) *}
-
-text {*
-  \begin{mldecls}
-  @{index_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\
-  @{index_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
-  @{index_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\
-  @{index_ML merge: "('a * 'a -> bool) -> 'a list * 'a list -> 'a list"} \\
-  \end{mldecls}
-*}
-
-text {*
-  Lists are often used as set-like data structures -- set-like in
-  the sense that they support a notion of @{ML member}-ship,
-  @{ML insert}-ing and @{ML remove}-ing, but are order-sensitive.
-  This is convenient when implementing a history-like mechanism:
-  @{ML insert} adds an element \emph{to the front} of a list,
-  if not yet present; @{ML remove} removes \emph{all} occurences
-  of a particular element.  Correspondingly @{ML merge} implements a 
-  a merge on two lists suitable for merges of context data
-  (\secref{sec:context-theory}).
-
-  Functions are parametrized by an explicit equality function
-  to accomplish overloaded equality;  in most cases of monomorphic
-  equality, writing @{ML "op ="} should suffice.
-*}
-
 subsection {* Association lists *}
 
 text {*