# HG changeset patch
# User haftmann
# Date 1162907349 -3600
# Node ID 6dfdb69e83ef0523d0439319fc5016885cd874c1
# Parent  ef30d1e6f03a2763d3d0ad30627ac2dcca5b8ef2
adjusted title

diff -r ef30d1e6f03a -r 6dfdb69e83ef doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- 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
diff -r ef30d1e6f03a -r 6dfdb69e83ef doc-src/IsarAdvanced/Codegen/codegen.tex
--- 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}}