--- a/doc-src/IsarImplementation/Thy/ML.thy Thu Mar 27 15:32:19 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Thu Mar 27 16:24:10 2008 +0100
@@ -2,7 +2,7 @@
theory "ML" imports base begin
-chapter {* Aesthetics of ML programming *}
+chapter {* Advanced ML programming *}
section {* Style *}
@@ -626,10 +626,4 @@
*}
-chapter {* Cookbook *}
-
-section {* A method that depends on declarations in the context *}
-
-text FIXME
-
end
--- 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