diff -r b416573f1807 -r 3dd426ae6bea doc-src/Codegen/Thy/Introduction.thy --- a/doc-src/Codegen/Thy/Introduction.thy Wed Oct 19 22:54:26 2011 +0200 +++ b/doc-src/Codegen/Thy/Introduction.thy Wed Oct 19 23:07:48 2011 +0200 @@ -236,15 +236,6 @@ \begin{center}\textit{Happy proving, happy hacking!}\end{center} \end{minipage}}}\end{center} - - \begin{warn} - There is also a more ancient code generator in Isabelle by Stefan - Berghofer \cite{Berghofer-Nipkow:2002}. Although its - functionality is covered by the code generator presented here, it - will sometimes show up as an artifact. In case of ambiguity, we - will refer to the framework described here as @{text "generic code - generator"}, to the other as @{text "SML code generator"}. - \end{warn} *} end