# HG changeset patch
# User haftmann
# Date 1239087163 -7200
# Node ID 257cbe43faa8385dc9641d87d7407f5fb45490ee
# Parent  efcba7788b2eb039835f005464456e53f6dab8d3
tuned manual

diff -r efcba7788b2e -r 257cbe43faa8 doc-src/Codegen/Thy/Adaption.thy
--- 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 {*
diff -r efcba7788b2e -r 257cbe43faa8 doc-src/Codegen/Thy/Further.thy
--- 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)) =
diff -r efcba7788b2e -r 257cbe43faa8 doc-src/Codegen/Thy/Introduction.thy
--- 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}
 
diff -r efcba7788b2e -r 257cbe43faa8 doc-src/Codegen/Thy/document/Adaption.tex
--- 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
diff -r efcba7788b2e -r 257cbe43faa8 doc-src/Codegen/Thy/document/Further.tex
--- 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
diff -r efcba7788b2e -r 257cbe43faa8 doc-src/Codegen/Thy/document/Introduction.tex
--- 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}