diff -r cc6768509ed3 -r 33137422d7fd doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Tue Sep 18 08:28:47 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Tue Sep 18 10:44:02 2007 +0200 @@ -1198,7 +1198,7 @@ \end{description} *} -subsubsection {* Datatype hooks *} +(*subsubsection {* Datatype hooks *} text {* Isabelle/HOL's datatype package provides a mechanism to @@ -1311,7 +1311,9 @@ the block. \end{description} +*}*) +text {* \emph{Happy proving, happy hacking!} *}