1.1 --- a/doc-src/Codegen/Thy/Adaption.thy	Mon Apr 06 15:59:20 2009 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Adaption.thy	Tue Apr 07 08:52:43 2009 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4  subsection {* The adaption principle *}
     1.5  
     1.6  text {*
     1.7 -  The following figure illustrates what \qt{adaption} is conceptually
     1.8 +  Figure \ref{fig:adaption} illustrates what \qt{adaption} is conceptually
     1.9    supposed to be:
    1.10  
    1.11    \begin{figure}[here]
    1.12 @@ -287,8 +287,9 @@
    1.13  
    1.14  instance %quote by default (simp add: eq_bar_def)
    1.15  
    1.16 -end %quote
    1.17 -code_type %quotett bar
    1.18 +end %quote (*<*)
    1.19 +
    1.20 +(*>*) code_type %quotett bar
    1.21    (Haskell "Integer")
    1.22  
    1.23  text {*

     2.1 --- a/doc-src/Codegen/Thy/Further.thy	Mon Apr 06 15:59:20 2009 +0200
     2.2 +++ b/doc-src/Codegen/Thy/Further.thy	Tue Apr 07 08:52:43 2009 +0200
     2.3 @@ -78,8 +78,9 @@
     2.4    with system code, the code generator provides a @{text code} antiquotation:
     2.5  *}
     2.6  
     2.7 -datatype %quote form = T | F | And form form | Or form form
     2.8 -ML %quotett {*
     2.9 +datatype %quote form = T | F | And form form | Or form form (*<*)
    2.10 +
    2.11 +(*>*) ML %quotett {*
    2.12    fun eval_form @{code T} = true
    2.13      | eval_form @{code F} = false
    2.14      | eval_form (@{code And} (p, q)) =

     3.1 --- a/doc-src/Codegen/Thy/Introduction.thy	Mon Apr 06 15:59:20 2009 +0200
     3.2 +++ b/doc-src/Codegen/Thy/Introduction.thy	Tue Apr 07 08:52:43 2009 +0200
     3.3 @@ -138,7 +138,7 @@
     3.4    into a functional program.  This is achieved by three major
     3.5    components which operate sequentially, i.e. the result of one is
     3.6    the input
     3.7 -  of the next in the chain,  see diagram \ref{fig:arch}:
     3.8 +  of the next in the chain,  see figure \ref{fig:arch}:
     3.9  
    3.10    \begin{itemize}
    3.11  

     4.1 --- a/doc-src/Codegen/Thy/document/Adaption.tex	Mon Apr 06 15:59:20 2009 +0200
     4.2 +++ b/doc-src/Codegen/Thy/document/Adaption.tex	Tue Apr 07 08:52:43 2009 +0200
     4.3 @@ -92,7 +92,7 @@
     4.4  \isamarkuptrue%
     4.5  %
     4.6  \begin{isamarkuptext}%
     4.7 -The following figure illustrates what \qt{adaption} is conceptually
     4.8 +Figure \ref{fig:adaption} illustrates what \qt{adaption} is conceptually
     4.9    supposed to be:
    4.10  
    4.11    \begin{figure}[here]
    4.12 @@ -545,10 +545,9 @@
    4.13  \isadelimquote
    4.14  %
    4.15  \endisadelimquote
    4.16 -\isanewline
    4.17  %
    4.18  \isadelimquotett
    4.19 -%
    4.20 +\ %
    4.21  \endisadelimquotett
    4.22  %
    4.23  \isatagquotett

     5.1 --- a/doc-src/Codegen/Thy/document/Further.tex	Mon Apr 06 15:59:20 2009 +0200
     5.2 +++ b/doc-src/Codegen/Thy/document/Further.tex	Tue Apr 07 08:52:43 2009 +0200
     5.3 @@ -154,17 +154,16 @@
     5.4  %
     5.5  \isatagquote
     5.6  \isacommand{datatype}\isamarkupfalse%
     5.7 -\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form%
     5.8 +\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
     5.9  \endisatagquote
    5.10  {\isafoldquote}%
    5.11  %
    5.12  \isadelimquote
    5.13  %
    5.14  \endisadelimquote
    5.15 -\isanewline
    5.16  %
    5.17  \isadelimquotett
    5.18 -%
    5.19 +\ %
    5.20  \endisadelimquotett
    5.21  %
    5.22  \isatagquotett

     6.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex	Mon Apr 06 15:59:20 2009 +0200
     6.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Apr 07 08:52:43 2009 +0200
     6.3 @@ -301,7 +301,7 @@
     6.4    into a functional program.  This is achieved by three major
     6.5    components which operate sequentially, i.e. the result of one is
     6.6    the input
     6.7 -  of the next in the chain,  see diagram \ref{fig:arch}:
     6.8 +  of the next in the chain,  see figure \ref{fig:arch}:
     6.9  
    6.10    \begin{itemize}
    6.11