--- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Oct 19 22:54:26 2011 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Oct 19 23:07:48 2011 +0200
@@ -560,15 +560,7 @@
\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 \isa{generic\ code\ generator}, to the other as \isa{SML\ code\ generator}.
- \end{warn}%
+ \end{minipage}}}\end{center}%
\end{isamarkuptext}%
\isamarkuptrue%
%