--- 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%
%