# HG changeset patch
# User wenzelm
# Date 1136243183 -3600
# Node ID e903a1d0bed58dd255475ccb05ac14a680378da3
# Parent  f42e544805f549f96d2f85b0a0d1da12c3837764
updated;

diff -r f42e544805f5 -r e903a1d0bed5 doc-src/IsarImplementation/Thy/document/ML.tex
--- 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