--- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue Jan 03 00:06:22 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue Jan 03 00:06:23 2006 +0100
@@ -4,20 +4,53 @@
%
\isadelimtheory
\isanewline
+\isanewline
+\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
-\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ Pure\ \isakeyword{begin}\ \isacommand{end}\isamarkupfalse%
+\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Aesthetics of ML programming%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME style guide%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupchapter{Basic library functions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME beyond the basis library definition%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
-\isanewline
%
\endisadelimtheory
+\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex