--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Tue Nov 07 14:30:03 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Tue Nov 07 14:49:09 2006 +0100
@@ -425,7 +425,7 @@
\item the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}
for exhaustive syntax diagrams.
- \item or \fixme{ref} which deals with foundational issues
+ \item or \fixme[ref] which deals with foundational issues
of the code generator framework.
\end{itemize}
@@ -1371,6 +1371,8 @@
a final state yet.
Changes likely to occur in future.
\end{warn}
+
+ \fixme
*}
subsubsection {* Data depending on the theory's executable content *}
@@ -1443,8 +1445,9 @@
\end{mldecls}
*}
-(*text {*
- \emph{Happy proving, happy hacking!}
-*}*)
+text {*
+ \fixme
+% \emph{Happy proving, happy hacking!}
+*}
end
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex Tue Nov 07 14:30:03 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Tue Nov 07 14:49:09 2006 +0100
@@ -63,7 +63,7 @@
\isadroptag{theory}
\title{\includegraphics[scale=0.5]{isabelle_isar}
- \\[4ex] Code generation from Isabelle theories}
+ \\[4ex] Code generation from Isabelle/HOL theories}
\author{\emph{Florian Haftmann}}