--- a/doc-src/Codegen/Thy/document/Refinement.tex Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Mon Sep 27 16:27:31 2010 +0200
@@ -65,11 +65,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
@@ -79,12 +79,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent A more efficient implementation would use dynamic
@@ -161,11 +161,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline
@@ -180,12 +180,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\isamarkupsubsection{Datatype refinement%
}
@@ -337,11 +337,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -380,12 +380,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
The same techniques can also be applied to types which are not
@@ -571,11 +571,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -609,12 +609,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
Typical data structures implemented by representations involving