--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Dec 20 14:33:43 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Thu Dec 20 21:09:38 2007 +0100
@@ -461,7 +461,7 @@
\ \ {\isachardoublequoteopen}head\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ null{\isachardoublequoteclose}\isanewline
\ \ {\isacharbar}\ {\isachardoublequoteopen}head\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-We provide some instances for our \isa{null}:%
+\noindent We provide some instances for our \isa{null}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{instantiation}\isamarkupfalse%
@@ -474,7 +474,7 @@
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}null\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
%
@@ -496,7 +496,7 @@
\isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
-Constructing a dummy example:%
+\noindent Constructing a dummy example:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%