1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Wed Dec 05 04:34:15 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Wed Dec 05 14:15:39 2007 +0100
     1.3 @@ -464,9 +464,20 @@
     1.4  We provide some instances for our \isa{null}:%
     1.5  \end{isamarkuptext}%
     1.6  \isamarkuptrue%
     1.7 +\isacommand{instantiation}\isamarkupfalse%
     1.8 +\ option\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline
     1.9 +\isakeyword{begin}\isanewline
    1.10 +\isanewline
    1.11 +\isacommand{definition}\isamarkupfalse%
    1.12 +\isanewline
    1.13 +\ \ {\isachardoublequoteopen}null\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
    1.14 +\isanewline
    1.15 +\isacommand{definition}\isamarkupfalse%
    1.16 +\isanewline
    1.17 +\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
    1.18 +\isanewline
    1.19  \isacommand{instance}\isamarkupfalse%
    1.20 -\ option\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline
    1.21 -\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ None{\isachardoublequoteclose}%
    1.22 +%
    1.23  \isadelimproof
    1.24  \ %
    1.25  \endisadelimproof
    1.26 @@ -482,22 +493,7 @@
    1.27  \endisadelimproof
    1.28  \isanewline
    1.29  \isanewline
    1.30 -\isacommand{instance}\isamarkupfalse%
    1.31 -\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline
    1.32 -\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}%
    1.33 -\isadelimproof
    1.34 -\ %
    1.35 -\endisadelimproof
    1.36 -%
    1.37 -\isatagproof
    1.38 -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
    1.39 -%
    1.40 -\endisatagproof
    1.41 -{\isafoldproof}%
    1.42 -%
    1.43 -\isadelimproof
    1.44 -%
    1.45 -\endisadelimproof
    1.46 +\isacommand{end}\isamarkupfalse%
    1.47  %
    1.48  \begin{isamarkuptext}%
    1.49  Constructing a dummy example:%