diff -r baee64dbe8ea -r d53664118418 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Mar 22 16:53:37 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Fri Mar 23 09:40:43 2007 +0100
@@ -334,11 +334,6 @@
 }
 \isamarkuptrue%
 %
-\begin{isamarkuptext}%
-FIXME chronicle%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsubsection{Lists (as set-like data structures)%
 }
 \isamarkuptrue%
@@ -354,7 +349,19 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+Lists are often used as set-like data structures -- set-like in
+  then sense that they support notion of \verb|member|-ship,
+  \verb|insert|-ing and \verb|remove|-ing, but are order-sensitive.
+  This is convenient when implementing a history-like mechanism:
+  \verb|insert| adds an element \emph{to the front} of a list,
+  if not yet present; \verb|remove| removes \emph{all} occurences
+  of a particular element.  Correspondingly \verb|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 \verb|(op =)| should suffice.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -383,7 +390,20 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+Association lists can be seens as an extension of set-like lists:
+  on the one hand, they may be used to implement finite mappings,
+  on the other hand, they remain order-sensitive and allow for
+  multiple key-value-pair with the same key: \verb|AList.lookup|
+  returns the \emph{first} value corresponding to a particular
+  key, if present.  \verb|AList.update| updates
+  the \emph{first} occurence of a particular key; if no such
+  key exists yet, the key-value-pair is added \emph{to the front}.
+  \verb|AList.delete| only deletes the \emph{first} occurence of a key.
+  \verb|AList.merge| provides an operation suitable for merges of context data
+  (\secref{sec:context-theory}), where an equality parameter on
+  values determines whether a merge should be considered a conflict.
+  A slightly generalized operation if implementend by the \verb|AList.join|
+  function which allows for explicit conflict resolution.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -423,7 +443,17 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+Tables are an efficient representation of finite mappings without
+  any notion of order;  due to their efficiency they should be used
+  whenever such pure finite mappings are neccessary.
+
+  The key type of tables must be given explicitly by instantiating
+  the \verb|TableFun| functor which takes the key type
+  together with its \verb|order|; for convience, we restrict
+  here to the \verb|Symtab| instance with \verb|string|
+  as key type.
+
+  Most table functions correspond to those of association lists.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %