1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Mar 27 15:32:19 2008 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Thu Mar 27 16:24:10 2008 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4  
     1.5  theory "ML" imports base begin
     1.6  
     1.7 -chapter {* Aesthetics of ML programming *}
     1.8 +chapter {* Advanced ML programming *}
     1.9  
    1.10  section {* Style *}
    1.11  
    1.12 @@ -626,10 +626,4 @@
    1.13  *}
    1.14  
    1.15  
    1.16 -chapter {* Cookbook *}
    1.17 -
    1.18 -section {* A method that depends on declarations in the context *}
    1.19 -
    1.20 -text FIXME
    1.21 -
    1.22  end

     2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Mar 27 15:32:19 2008 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Mar 27 16:24:10 2008 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4  %
     2.5  \endisadelimtheory
     2.6  %
     2.7 -\isamarkupchapter{Aesthetics of ML programming%
     2.8 +\isamarkupchapter{Advanced ML programming%
     2.9  }
    2.10  \isamarkuptrue%
    2.11  %
    2.12 @@ -381,7 +381,7 @@
    2.13  
    2.14    Written with naive application, an addition of constant
    2.15    \isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and
    2.16 -  a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like:
    2.17 +  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:
    2.18  
    2.19    \begin{quotation}
    2.20     \verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
    2.21 @@ -773,19 +773,6 @@
    2.22  \end{isamarkuptext}%
    2.23  \isamarkuptrue%
    2.24  %
    2.25 -\isamarkupchapter{Cookbook%
    2.26 -}
    2.27 -\isamarkuptrue%
    2.28 -%
    2.29 -\isamarkupsection{A method that depends on declarations in the context%
    2.30 -}
    2.31 -\isamarkuptrue%
    2.32 -%
    2.33 -\begin{isamarkuptext}%
    2.34 -FIXME%
    2.35 -\end{isamarkuptext}%
    2.36 -\isamarkuptrue%
    2.37 -%
    2.38  \isadelimtheory
    2.39  %
    2.40  \endisadelimtheory