doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
changeset 24628 33137422d7fd
parent 24421 acfb2413faa3
child 24994 c385c4eabb3b
--- 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!}
 *}