--- a/doc-src/IsarImplementation/Thy/document/ML.tex Thu Mar 27 15:32:19 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu Mar 27 16:24:10 2008 +0100
@@ -18,7 +18,7 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Aesthetics of ML programming%
+\isamarkupchapter{Advanced ML programming%
}
\isamarkuptrue%
%
@@ -381,7 +381,7 @@
Written with naive application, an addition of constant
\isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and
- a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like:
+ a corresponding definition \isa{bar{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}{\isacharbraceright}\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}{\isacharbraceright}\ {\isasymequiv}\ {\isasymlambda}x{\isasymColon}{\isacharprime}a{\isasymColon}{\isacharbraceleft}{\isacharbraceright}{\isachardot}\ x} would look like:
\begin{quotation}
\verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
@@ -773,19 +773,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupchapter{Cookbook%
-}
-\isamarkuptrue%
-%
-\isamarkupsection{A method that depends on declarations in the context%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isadelimtheory
%
\endisadelimtheory