# HG changeset patch
# User wenzelm
# Date 1206631450 -3600
# Node ID 5906619c8c6b345fa4272f5b237478b4c4ccef5f
# Parent  dfd6947ab5c29131078ef5ab0ff3eaefc620adae
tuned appendix;

diff -r dfd6947ab5c2 -r 5906619c8c6b doc-src/IsarImplementation/Thy/ML.thy
--- 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
diff -r dfd6947ab5c2 -r 5906619c8c6b doc-src/IsarImplementation/Thy/document/ML.tex
--- 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