doc-src/IsarAdvanced/Codegen/Thy/ML.thy
changeset 28447 df77ed974a78
parent 28419 f65e8b318581
child 28635 cc53d2ab0170
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/ML.thy	Wed Oct 01 12:18:18 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/ML.thy	Wed Oct 01 13:33:54 2008 +0200
     1.3 @@ -108,12 +108,6 @@
     1.4    involves using those primitive interfaces
     1.5    but also storing code-dependent data and various
     1.6    other things.
     1.7 -
     1.8 -  \begin{warn}
     1.9 -    Some interfaces discussed here have not reached
    1.10 -    a final state yet.
    1.11 -    Changes likely to occur in future.
    1.12 -  \end{warn}
    1.13  *}
    1.14  
    1.15  subsubsection {* Data depending on the theory's executable content *}
    1.16 @@ -152,7 +146,7 @@
    1.17  
    1.18    \end{description}
    1.19  
    1.20 -  An instance of @{ML_functor CodeDataFun} provides the following
    1.21 +  \noindent An instance of @{ML_functor CodeDataFun} provides the following
    1.22    interface:
    1.23  
    1.24    \medskip
    1.25 @@ -175,6 +169,8 @@
    1.26  *}
    1.27  
    1.28  text {*
    1.29 +  \bigskip
    1.30 +
    1.31    \emph{Happy proving, happy hacking!}
    1.32  *}
    1.33