diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/document/Foundations.tex
--- a/doc-src/Codegen/Thy/document/Foundations.tex	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex	Mon Sep 27 16:27:31 2010 +0200
@@ -238,11 +238,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
@@ -253,12 +253,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has
@@ -338,11 +338,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -373,12 +373,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent Obviously, polymorphic equality is implemented the Haskell
@@ -431,11 +431,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
@@ -447,12 +447,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent In some cases it is desirable to have this
@@ -520,11 +520,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a{\isacharsemicolon}\isanewline
@@ -538,12 +538,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent This feature however is rarely needed in practice.  Note