--- a/doc-src/Codegen/Thy/Adaption.thy Mon Apr 06 15:59:20 2009 +0200
+++ b/doc-src/Codegen/Thy/Adaption.thy Tue Apr 07 08:52:43 2009 +0200
@@ -55,7 +55,7 @@
subsection {* The adaption principle *}
text {*
- The following figure illustrates what \qt{adaption} is conceptually
+ Figure \ref{fig:adaption} illustrates what \qt{adaption} is conceptually
supposed to be:
\begin{figure}[here]
@@ -287,8 +287,9 @@
instance %quote by default (simp add: eq_bar_def)
-end %quote
-code_type %quotett bar
+end %quote (*<*)
+
+(*>*) code_type %quotett bar
(Haskell "Integer")
text {*
--- a/doc-src/Codegen/Thy/Further.thy Mon Apr 06 15:59:20 2009 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Tue Apr 07 08:52:43 2009 +0200
@@ -78,8 +78,9 @@
with system code, the code generator provides a @{text code} antiquotation:
*}
-datatype %quote form = T | F | And form form | Or form form
-ML %quotett {*
+datatype %quote form = T | F | And form form | Or form form (*<*)
+
+(*>*) ML %quotett {*
fun eval_form @{code T} = true
| eval_form @{code F} = false
| eval_form (@{code And} (p, q)) =
--- a/doc-src/Codegen/Thy/Introduction.thy Mon Apr 06 15:59:20 2009 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Tue Apr 07 08:52:43 2009 +0200
@@ -138,7 +138,7 @@
into a functional program. This is achieved by three major
components which operate sequentially, i.e. the result of one is
the input
- of the next in the chain, see diagram \ref{fig:arch}:
+ of the next in the chain, see figure \ref{fig:arch}:
\begin{itemize}
--- a/doc-src/Codegen/Thy/document/Adaption.tex Mon Apr 06 15:59:20 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Adaption.tex Tue Apr 07 08:52:43 2009 +0200
@@ -92,7 +92,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The following figure illustrates what \qt{adaption} is conceptually
+Figure \ref{fig:adaption} illustrates what \qt{adaption} is conceptually
supposed to be:
\begin{figure}[here]
@@ -545,10 +545,9 @@
\isadelimquote
%
\endisadelimquote
-\isanewline
%
\isadelimquotett
-%
+\ %
\endisadelimquotett
%
\isatagquotett
--- a/doc-src/Codegen/Thy/document/Further.tex Mon Apr 06 15:59:20 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Tue Apr 07 08:52:43 2009 +0200
@@ -154,17 +154,16 @@
%
\isatagquote
\isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form%
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
-\isanewline
%
\isadelimquotett
-%
+\ %
\endisadelimquotett
%
\isatagquotett
--- a/doc-src/Codegen/Thy/document/Introduction.tex Mon Apr 06 15:59:20 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Apr 07 08:52:43 2009 +0200
@@ -301,7 +301,7 @@
into a functional program. This is achieved by three major
components which operate sequentially, i.e. the result of one is
the input
- of the next in the chain, see diagram \ref{fig:arch}:
+ of the next in the chain, see figure \ref{fig:arch}:
\begin{itemize}