# HG changeset patch
# User haftmann
# Date 1285597651 -7200
# Node ID 3aa2bc9c5478e8374b3ca8d0b2229fbeb9f86973
# Parent  4e586b734facc55efa2f03da6b18f8e365773295
combine quote and typewriter/tt tag

diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/Adaptation.thy
--- a/doc-src/Codegen/Thy/Adaptation.thy	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy	Mon Sep 27 16:27:31 2010 +0200
@@ -175,7 +175,7 @@
 code_const %invisible True and False and "op \<and>" and Not
   (SML and and and)
 (*>*)
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts in_interval (SML)}
 *}
 
@@ -190,9 +190,9 @@
   "bool"}, we may use \qn{custom serialisations}:
 *}
 
-code_type %quote %tt bool
+code_type %quotett bool
   (SML "bool")
-code_const %quote %tt True and False and "op \<and>"
+code_const %quotett True and False and "op \<and>"
   (SML "true" and "false" and "_ andalso _")
 
 text {*
@@ -206,7 +206,7 @@
   placeholder for the type constructor's (the constant's) arguments.
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts in_interval (SML)}
 *}
 
@@ -218,10 +218,10 @@
   precedences which may be used here:
 *}
 
-code_const %quote %tt "op \<and>"
+code_const %quotett "op \<and>"
   (SML infixl 1 "andalso")
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts in_interval (SML)}
 *}
 
@@ -247,9 +247,9 @@
 code_const %invisible Pair
   (SML)
 (*>*)
-code_type %quote %tt prod
+code_type %quotett prod
   (SML infix 2 "*")
-code_const %quote %tt Pair
+code_const %quotett Pair
   (SML "!((_),/ (_))")
 
 text {*
@@ -283,10 +283,10 @@
   @{command_def code_class}) and its operation @{const [source] HOL.equal}
 *}
 
-code_class %quote %tt equal
+code_class %quotett equal
   (Haskell "Eq")
 
-code_const %quote %tt "HOL.equal"
+code_const %quotett "HOL.equal"
   (Haskell infixl 4 "==")
 
 text {*
@@ -307,7 +307,7 @@
 
 end %quote (*<*)
 
-(*>*) code_type %quote %tt bar
+(*>*) code_type %quotett bar
   (Haskell "Integer")
 
 text {*
@@ -316,7 +316,7 @@
   suppress this additional instance, use @{command_def "code_instance"}:
 *}
 
-code_instance %quote %tt bar :: equal
+code_instance %quotett bar :: equal
   (Haskell -)
 
 
@@ -328,10 +328,10 @@
   "code_include"} command:
 *}
 
-code_include %quote %tt Haskell "Errno"
+code_include %quotett Haskell "Errno"
 {*errno i = error ("Error number: " ++ show i)*}
 
-code_reserved %quote %tt Haskell Errno
+code_reserved %quotett Haskell Errno
 
 text {*
   \noindent Such named @{text include}s are then prepended to every
diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/Evaluation.thy
--- a/doc-src/Codegen/Thy/Evaluation.thy	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy	Mon Sep 27 16:27:31 2010 +0200
@@ -206,7 +206,7 @@
 
 datatype %quote form = T | F | And form form | Or form form (*<*)
 
-(*>*) ML %tt %quote {*
+(*>*) ML %quotett {*
   fun eval_form @{code T} = true
     | eval_form @{code F} = false
     | eval_form (@{code And} (p, q)) =
diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/Foundations.thy
--- a/doc-src/Codegen/Thy/Foundations.thy	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy	Mon Sep 27 16:27:31 2010 +0200
@@ -161,7 +161,7 @@
   is determined syntactically.  The resulting code:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts dequeue (consts) dequeue (Haskell)}
 *}
 
@@ -217,7 +217,7 @@
   equality check, as can be seen in the corresponding @{text SML} code:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts collect_duplicates (SML)}
 *}
 
@@ -255,7 +255,7 @@
   for the pattern @{term "AQueue [] []"}:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
 *}
 
@@ -296,7 +296,7 @@
   exception at the appropriate position:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
 *}
 
diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/Further.thy
--- a/doc-src/Codegen/Thy/Further.thy	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy	Mon Sep 27 16:27:31 2010 +0200
@@ -112,7 +112,7 @@
   After this setup procedure, code generation can continue as usual:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
 *}
 
diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/Introduction.thy
--- a/doc-src/Codegen/Thy/Introduction.thy	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy	Mon Sep 27 16:27:31 2010 +0200
@@ -70,7 +70,7 @@
 
 text {* \noindent resulting in the following code: *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts empty enqueue dequeue (SML)}
 *}
 
@@ -93,7 +93,7 @@
   \noindent This is the corresponding code:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts empty enqueue dequeue (Haskell)}
 *}
 
@@ -168,7 +168,7 @@
   native classes:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts bexp (Haskell)}
 *}
 
@@ -178,7 +178,7 @@
   @{text SML}:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts bexp (SML)}
 *}
 
diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/Refinement.thy
--- a/doc-src/Codegen/Thy/Refinement.thy	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy	Mon Sep 27 16:27:31 2010 +0200
@@ -31,7 +31,7 @@
   to two recursive calls:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts fib (consts) fib (Haskell)}
 *}
 
@@ -69,7 +69,7 @@
   \noindent The resulting code shows only linear growth of runtime:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts fib (consts) fib fib_step (Haskell)}
 *}
 
@@ -157,7 +157,7 @@
   \noindent The resulting code looks as expected:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts empty enqueue dequeue (SML)}
 *}
 
@@ -253,7 +253,7 @@
   \noindent Then the corresponding code is as follows:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
 *} (*(types) dlist (consts) dempty dinsert dremove list_of List.member insert remove *)
 
diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Mon Sep 27 16:27:31 2010 +0200
@@ -228,11 +228,11 @@
 %
 \endisadeliminvisible
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -264,12 +264,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent Though this is correct code, it is a little bit
@@ -281,23 +281,23 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
-\isatagtt
+\isatagquotett
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ bool\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
 \begin{isamarkuptext}%
 \noindent The \indexdef{}{command}{code\_type}\hypertarget{command.code-type}{\hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} command takes a type constructor
@@ -311,11 +311,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -338,12 +338,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent This still is not perfect: the parentheses around the
@@ -354,26 +354,26 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
-\isatagtt
+\isatagquotett
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -396,12 +396,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent The attentive reader may ask how we assert that no
@@ -447,23 +447,23 @@
 %
 \endisadeliminvisible
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
-\isatagtt
+\isatagquotett
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ prod\isanewline
 \ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ Pair\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
 \begin{isamarkuptext}%
 \noindent The initial bang ``\verb|!|'' tells the serialiser
@@ -499,11 +499,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
-\isatagtt
+\isatagquotett
 \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
 \ equal\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
@@ -511,12 +511,12 @@
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}HOL{\isachardot}equal{\isachardoublequoteclose}\isanewline
 \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
 \begin{isamarkuptext}%
 \noindent A problem now occurs whenever a type which is an instance
@@ -553,20 +553,20 @@
 %
 \endisadelimquote
 %
-\isadelimtt
+\isadelimquotett
 \ %
-\endisadelimtt
+\endisadelimquotett
 %
-\isatagtt
+\isatagquotett
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ bar\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
 \begin{isamarkuptext}%
 \noindent The code generator would produce an additional instance,
@@ -575,20 +575,20 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
-\isatagtt
+\isatagquotett
 \isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
 \ bar\ {\isacharcolon}{\isacharcolon}\ equal\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
 \isamarkupsubsection{Enhancing the target language context \label{sec:include}%
 }
@@ -600,23 +600,23 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
-\isatagtt
+\isatagquotett
 \isacommand{code{\isacharunderscore}include}\isamarkupfalse%
 \ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline
 {\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
 \ Haskell\ Errno%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
 \begin{isamarkuptext}%
 \noindent Such named \isa{include}s are then prepended to every
diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/document/Evaluation.tex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Mon Sep 27 16:27:31 2010 +0200
@@ -269,7 +269,20 @@
 %
 \isatagquote
 \isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ \ \isacommand{ML}\isamarkupfalse%
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isadelimquotett
+\ %
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{ML}\isamarkupfalse%
 \ {\isacharverbatimopen}\isanewline
 \ \ fun\ eval{\isacharunderscore}form\ %
 \isaantiq
@@ -294,12 +307,12 @@
 \ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
 \ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
 {\isacharverbatimclose}%
-\endisatagquote
-{\isafoldquote}%
+\endisatagquotett
+{\isafoldquotett}%
 %
-\isadelimquote
+\isadelimquotett
 %
-\endisadelimquote
+\endisadelimquotett
 %
 \begin{isamarkuptext}%
 \noindent \isa{code} takes as argument the name of a constant;
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
diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/document/Further.tex
--- a/doc-src/Codegen/Thy/document/Further.tex	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex	Mon Sep 27 16:27:31 2010 +0200
@@ -207,11 +207,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 funpow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
@@ -224,12 +224,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \isamarkupsubsection{Imperative data structures%
 }
diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Mon Sep 27 16:27:31 2010 +0200
@@ -133,11 +133,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -176,12 +176,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent The \indexdef{}{command}{export\_code}\hypertarget{command.export-code}{\hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}} command takes a
@@ -216,11 +216,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -245,12 +245,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent For more details about \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} see
@@ -382,11 +382,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -431,12 +431,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent This is a convenient place to show how explicit dictionary
@@ -445,11 +445,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -499,12 +499,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \begin{isamarkuptext}%
 \noindent Note the parameters with trailing underscore (\verb|A_|), which are the dictionary parameters.%
diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/document/Refinement.tex
--- 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