# HG changeset patch
# User haftmann
# Date 1223645013 -7200
# Node ID 1358b1ddd915ccee4401bbfd084be37b3aa0e5de
# Parent  21b3a00a3ff0192558d79935a63cd01d8cfd1377
tuned

diff -r 21b3a00a3ff0 -r 1358b1ddd915 doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Fri Oct 10 06:49:44 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Fri Oct 10 15:23:33 2008 +0200
@@ -116,7 +116,7 @@
   SML code:
 *}
 
-primrec %quoteme in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
+primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
   "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
 (*<*)
 code_type %invisible bool
@@ -124,7 +124,7 @@
 code_const %invisible True and False and "op \<and>" and Not
   (SML and and and)
 (*>*)
-text %quoteme {*@{code_stmts in_interval (SML)}*}
+text %quote {*@{code_stmts in_interval (SML)}*}
 
 text {*
   \noindent Though this is correct code, it is a little bit unsatisfactory:
@@ -138,9 +138,9 @@
   \qn{custom serialisations}:
 *}
 
-code_type %tt bool
+code_type %quotett bool
   (SML "bool")
-code_const %tt True and False and "op \<and>"
+code_const %quotett True and False and "op \<and>"
   (SML "true" and "false" and "_ andalso _")
 
 text {*
@@ -155,7 +155,7 @@
   for the type constructor's (the constant's) arguments.
 *}
 
-text %quoteme {*@{code_stmts in_interval (SML)}*}
+text %quote {*@{code_stmts in_interval (SML)}*}
 
 text {*
   \noindent This still is not perfect: the parentheses
@@ -166,10 +166,10 @@
   associative infixes with precedences which may be used here:
 *}
 
-code_const %tt "op \<and>"
+code_const %quotett "op \<and>"
   (SML infixl 1 "andalso")
 
-text %quoteme {*@{code_stmts in_interval (SML)}*}
+text %quote {*@{code_stmts in_interval (SML)}*}
 
 text {*
   \noindent The attentive reader may ask how we assert that no generated
@@ -180,7 +180,7 @@
   accidental overwrites, using the @{command "code_reserved"} command:
 *}
 
-code_reserved %quoteme "SML " bool true false andalso
+code_reserved %quote "SML " bool true false andalso
 
 text {*
   \noindent Next, we try to map HOL pairs to SML pairs, using the
@@ -192,9 +192,9 @@
 code_const %invisible Pair
   (SML)
 (*>*)
-code_type %tt *
+code_type %quotett *
   (SML infix 2 "*")
-code_const %tt Pair
+code_const %quotett Pair
   (SML "!((_),/ (_))")
 
 text {*
@@ -232,10 +232,10 @@
   @{const HOL.eq}
 *}
 
-code_class %tt eq
+code_class %quotett eq
   (Haskell "Eq" where "HOL.eq" \<equiv> "(==)")
 
-code_const %tt "op ="
+code_const %quotett "op ="
   (Haskell infixl 4 "==")
 
 text {*
@@ -245,18 +245,18 @@
   of @{text Haskell} @{text Eq}:
 *}
 
-typedecl %quoteme bar
+typedecl %quote bar
 
-instantiation %quoteme bar :: eq
+instantiation %quote bar :: eq
 begin
 
-definition %quoteme "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
+definition %quote "eq_class.eq (x\<Colon>bar) y \<longleftrightarrow> x = y"
 
-instance %quoteme by default (simp add: eq_bar_def)
+instance %quote by default (simp add: eq_bar_def)
 
-end %quoteme
+end %quote
 
-code_type %tt bar
+code_type %quotett bar
   (Haskell "Integer")
 
 text {*
@@ -267,7 +267,7 @@
   @{text "code_instance"}:
 *}
 
-code_instance %tt bar :: eq
+code_instance %quotett bar :: eq
   (Haskell -)
 
 
@@ -279,10 +279,10 @@
   command:
 *}
 
-code_include %tt Haskell "Errno"
+code_include %quotett Haskell "Errno"
 {*errno i = error ("Error number: " ++ show i)*}
 
-code_reserved %tt Haskell Errno
+code_reserved %quotett Haskell Errno
 
 text {*
   \noindent Such named @{text include}s are then prepended to every generated code.
diff -r 21b3a00a3ff0 -r 1358b1ddd915 doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy	Fri Oct 10 06:49:44 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy	Fri Oct 10 15:23:33 2008 +0200
@@ -65,15 +65,15 @@
   For example, here a simple \qt{implementation} of amortised queues:
 *}
 
-datatype %quoteme 'a queue = Queue "'a list" "'a list"
+datatype %quote 'a queue = Queue "'a list" "'a list"
 
-definition %quoteme empty :: "'a queue" where
+definition %quote empty :: "'a queue" where
   "empty = Queue [] []"
 
-primrec %quoteme enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
+primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
   "enqueue x (Queue xs ys) = Queue (x # xs) ys"
 
-fun %quoteme dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
+fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
     "dequeue (Queue [] []) = (None, Queue [] [])"
   | "dequeue (Queue xs (y # ys)) = (Some y, Queue xs ys)"
   | "dequeue (Queue xs []) =
@@ -81,12 +81,12 @@
 
 text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *}
 
-export_code %quoteme empty dequeue enqueue in SML
+export_code %quote empty dequeue enqueue in SML
   module_name Example file "examples/example.ML"
 
 text {* \noindent resulting in the following code: *}
 
-text %quoteme {*@{code_stmts empty enqueue dequeue (SML)}*}
+text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
 
 text {*
   \noindent The @{command export_code} command takes a space-separated list of
@@ -100,14 +100,14 @@
   (with extension @{text ".hs"}) is written:
 *}
 
-export_code %quoteme empty dequeue enqueue in Haskell
+export_code %quote empty dequeue enqueue in Haskell
   module_name Example file "examples/"
 
 text {*
   \noindent This is how the corresponding code in @{text Haskell} looks like:
 *}
 
-text %quoteme {*@{code_stmts empty enqueue dequeue (Haskell)}*}
+text %quote {*@{code_stmts empty enqueue dequeue (Haskell)}*}
 
 text {*
   \noindent This demonstrates the basic usage of the @{command export_code} command;
diff -r 21b3a00a3ff0 -r 1358b1ddd915 doc-src/IsarAdvanced/Codegen/Thy/Program.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Fri Oct 10 06:49:44 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Fri Oct 10 15:23:33 2008 +0200
@@ -25,7 +25,7 @@
   explicitly:
 *}
 
-lemma %quoteme [code]:
+lemma %quote [code]:
   "dequeue (Queue xs []) =
      (if xs = [] then (None, Queue [] [])
        else dequeue (Queue [] (rev xs)))"
@@ -40,7 +40,7 @@
   the corresponding constant is determined syntactically.  The resulting code:
 *}
 
-text %quoteme {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
+text %quote {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
 
 text {*
   \noindent You may note that the equality test @{term "xs = []"} has been
@@ -56,7 +56,7 @@
   may be inspected using the @{command code_thms} command:
 *}
 
-code_thms %quoteme dequeue
+code_thms %quote dequeue
 
 text {*
   \noindent prints a table with \emph{all} defining equations
@@ -75,31 +75,31 @@
   from abstract algebra:
 *}
 
-class %quoteme semigroup = type +
+class %quote semigroup = type +
   fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
   assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
 
-class %quoteme monoid = semigroup +
+class %quote monoid = semigroup +
   fixes neutral :: 'a ("\<one>")
   assumes neutl: "\<one> \<otimes> x = x"
     and neutr: "x \<otimes> \<one> = x"
 
-instantiation %quoteme nat :: monoid
+instantiation %quote nat :: monoid
 begin
 
-primrec %quoteme mult_nat where
+primrec %quote mult_nat where
     "0 \<otimes> n = (0\<Colon>nat)"
   | "Suc m \<otimes> n = n + m \<otimes> n"
 
-definition %quoteme neutral_nat where
+definition %quote neutral_nat where
   "\<one> = Suc 0"
 
-lemma %quoteme add_mult_distrib:
+lemma %quote add_mult_distrib:
   fixes n m q :: nat
   shows "(n + m) \<otimes> q = n \<otimes> q + m \<otimes> q"
   by (induct n) simp_all
 
-instance %quoteme proof
+instance %quote proof
   fix m n q :: nat
   show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
     by (induct m) (simp_all add: add_mult_distrib)
@@ -109,14 +109,14 @@
     by (induct m) (simp_all add: neutral_nat_def)
 qed
 
-end %quoteme
+end %quote
 
 text {*
   \noindent We define the natural operation of the natural numbers
   on monoids:
 *}
 
-primrec %quoteme (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+primrec %quote (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
     "pow 0 a = \<one>"
   | "pow (Suc n) a = a \<otimes> pow n a"
 
@@ -124,21 +124,21 @@
   \noindent This we use to define the discrete exponentiation function:
 *}
 
-definition %quoteme bexp :: "nat \<Rightarrow> nat" where
+definition %quote bexp :: "nat \<Rightarrow> nat" where
   "bexp n = pow n (Suc (Suc 0))"
 
 text {*
   \noindent The corresponding code:
 *}
 
-text %quoteme {*@{code_stmts bexp (Haskell)}*}
+text %quote {*@{code_stmts bexp (Haskell)}*}
 
 text {*
   \noindent This is a convenient place to show how explicit dictionary construction
   manifests in generated code (here, the same example in @{text SML}):
 *}
 
-text %quoteme {*@{code_stmts bexp (SML)}*}
+text %quote {*@{code_stmts bexp (SML)}*}
 
 text {*
   \noindent Note the parameters with trailing underscore (@{verbatim "A_"})
@@ -173,21 +173,21 @@
      \item replacing non-executable constructs by executable ones:
 *}     
 
-lemma %quoteme [code inline]:
+lemma %quote [code inline]:
   "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
 
 text {*
      \item eliminating superfluous constants:
 *}
 
-lemma %quoteme [code inline]:
+lemma %quote [code inline]:
   "1 = Suc 0" by simp
 
 text {*
      \item replacing executable but inconvenient constructs:
 *}
 
-lemma %quoteme [code inline]:
+lemma %quote [code inline]:
   "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
 
 text_raw {*
@@ -236,10 +236,10 @@
     does something similar}.  First, the digit representation:
 *}
 
-definition %quoteme Dig0 :: "nat \<Rightarrow> nat" where
+definition %quote Dig0 :: "nat \<Rightarrow> nat" where
   "Dig0 n = 2 * n"
 
-definition %quoteme  Dig1 :: "nat \<Rightarrow> nat" where
+definition %quote  Dig1 :: "nat \<Rightarrow> nat" where
   "Dig1 n = Suc (2 * n)"
 
 text {*
@@ -247,7 +247,7 @@
   in binary digits, e.g.:
 *}
 
-lemma %quoteme 42: "42 = Dig0 (Dig1 (Dig0 (Dig1 (Dig0 1))))"
+lemma %quote 42: "42 = Dig0 (Dig1 (Dig0 (Dig1 (Dig0 1))))"
   by (simp add: Dig0_def Dig1_def)
 
 text {*
@@ -255,7 +255,7 @@
   the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
 *}
 
-lemma %quoteme plus_Dig [code]:
+lemma %quote plus_Dig [code]:
   "0 + n = n"
   "m + 0 = m"
   "1 + Dig0 n = Dig1 n"
@@ -274,7 +274,7 @@
   datatype constructors:
 *}
 
-code_datatype %quoteme "0\<Colon>nat" "1\<Colon>nat" Dig0 Dig1
+code_datatype %quote "0\<Colon>nat" "1\<Colon>nat" Dig0 Dig1
 
 text {*
   \noindent For the former constructor @{term Suc}, we provide a code
@@ -282,18 +282,18 @@
   which are an obstacle here:
 *}
 
-lemma %quoteme Suc_Dig [code]:
+lemma %quote Suc_Dig [code]:
   "Suc n = n + 1"
   by simp
 
-declare %quoteme One_nat_def [code inline del]
-declare %quoteme add_Suc_shift [code del] 
+declare %quote One_nat_def [code inline del]
+declare %quote add_Suc_shift [code del] 
 
 text {*
   \noindent This yields the following code:
 *}
 
-text %quoteme {*@{code_stmts "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" (SML)}*}
+text %quote {*@{code_stmts "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" (SML)}*}
 
 text {*
   \noindent From this example, it can be easily glimpsed that using own constructor sets
@@ -329,7 +329,7 @@
   by the code generator:
 *}
 
-primrec %quoteme collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+primrec %quote collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "collect_duplicates xs ys [] = xs"
   | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
       then if z \<in> set ys
@@ -343,7 +343,7 @@
   performs an explicit equality check.
 *}
 
-text %quoteme {*@{code_stmts collect_duplicates (SML)}*}
+text %quote {*@{code_stmts collect_duplicates (SML)}*}
 
 text {*
   \noindent Obviously, polymorphic equality is implemented the Haskell
@@ -364,21 +364,21 @@
   (also see theory @{theory Product_ord}):
 *}
 
-instantiation %quoteme "*" :: (order, order) order
+instantiation %quote "*" :: (order, order) order
 begin
 
-definition %quoteme [code del]:
+definition %quote [code del]:
   "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
 
-definition %quoteme [code del]:
+definition %quote [code del]:
   "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
 
-instance %quoteme proof
+instance %quote proof
 qed (auto simp: less_eq_prod_def less_prod_def intro: order_less_trans)
 
-end %quoteme
+end %quote
 
-lemma %quoteme order_prod [code]:
+lemma %quote order_prod [code]:
   "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
      x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
   "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
@@ -396,7 +396,7 @@
   code theorems:
 *}
 
-lemma %quoteme order_prod_code [code]:
+lemma %quote order_prod_code [code]:
   "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
      x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
   "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
@@ -407,7 +407,7 @@
   \noindent Then code generation succeeds:
 *}
 
-text %quoteme {*@{code_stmts "op \<le> \<Colon> _ \<times> _ \<Rightarrow> _ \<times> _ \<Rightarrow> bool" (SML)}*}
+text %quote {*@{code_stmts "op \<le> \<Colon> _ \<times> _ \<Rightarrow> _ \<times> _ \<Rightarrow> bool" (SML)}*}
 
 text {*
   In some cases, the automatically derived defining equations
@@ -417,7 +417,7 @@
   are referred to by natural numbers):
 *}
 
-datatype %quoteme monotype = Mono nat "monotype list"
+datatype %quote monotype = Mono nat "monotype list"
 (*<*)
 lemma monotype_eq:
   "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<equiv> 
@@ -438,7 +438,7 @@
   @{const [show_types] list_all2} can do the job:
 *}
 
-lemma %quoteme monotype_eq_list_all2 [code]:
+lemma %quote monotype_eq_list_all2 [code]:
   "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
      eq_class.eq tyco1 tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
   by (simp add: eq list_all2_eq [symmetric])
@@ -447,7 +447,7 @@
   \noindent does not depend on instance @{text "monotype \<Colon> eq"}:
 *}
 
-text %quoteme {*@{code_stmts "eq_class.eq :: monotype \<Rightarrow> monotype \<Rightarrow> bool" (SML)}*}
+text %quote {*@{code_stmts "eq_class.eq :: monotype \<Rightarrow> monotype \<Rightarrow> bool" (SML)}*}
 
 
 subsection {* Explicit partiality *}
@@ -457,7 +457,7 @@
   in the following example, again for amortised queues:
 *}
 
-fun %quoteme strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
+fun %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
   "strict_dequeue (Queue xs (y # ys)) = (y, Queue xs ys)"
   | "strict_dequeue (Queue xs []) =
       (case rev xs of y # ys \<Rightarrow> (y, Queue [] ys))"
@@ -467,23 +467,23 @@
   for the pattern @{term "Queue [] []"}:
 *}
 
-text %quoteme {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
+text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
 
 text {*
   \noindent In some cases it is desirable to have this
   pseudo-\qt{partiality} more explicitly, e.g.~as follows:
 *}
 
-axiomatization %quoteme empty_queue :: 'a
+axiomatization %quote empty_queue :: 'a
 
-function %quoteme strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
+function %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
   "strict_dequeue' (Queue xs []) = (if xs = [] then empty_queue
      else strict_dequeue' (Queue [] (rev xs)))"
   | "strict_dequeue' (Queue xs (y # ys)) =
        (y, Queue xs ys)"
 by pat_completeness auto
 
-termination %quoteme strict_dequeue'
+termination %quote strict_dequeue'
 by (relation "measure (\<lambda>q::'a queue. case q of Queue xs ys \<Rightarrow> length xs)") simp_all
 
 text {*
@@ -502,14 +502,14 @@
   that category explicitly, use @{command "code_abort"}:
 *}
 
-code_abort %quoteme empty_queue
+code_abort %quote empty_queue
 
 text {*
   \noindent Then the code generator will just insert an error or
   exception at the appropriate position:
 *}
 
-text %quoteme {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
+text %quote {*@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}*}
 
 text {*
   \noindent This feature however is rarely needed in practice.
diff -r 21b3a00a3ff0 -r 1358b1ddd915 doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Fri Oct 10 06:49:44 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Fri Oct 10 15:23:33 2008 +0200
@@ -159,20 +159,20 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{primrec}\isamarkupfalse%
 \ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \isadeliminvisible
 %
@@ -187,11 +187,11 @@
 %
 \endisadeliminvisible
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -219,12 +219,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent Though this is correct code, it is a little bit unsatisfactory:
@@ -239,23 +239,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 \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
@@ -270,11 +270,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -295,12 +295,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent This still is not perfect: the parentheses
@@ -312,26 +312,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
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -352,12 +352,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent The attentive reader may ask how we assert that no generated
@@ -369,19 +369,19 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
 \ {\isachardoublequoteopen}SML\ {\isachardoublequoteclose}\ bool\ true\ false\ andalso%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent Next, we try to map HOL pairs to SML pairs, using the
@@ -402,23 +402,23 @@
 %
 \endisadeliminvisible
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
-\isatagtt
+\isatagquotett
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ {\isacharasterisk}\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 serializer
@@ -458,11 +458,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
-\isatagtt
+\isatagquotett
 \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
 \ eq\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}HOL{\isachardot}eq{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
@@ -470,12 +470,12 @@
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ {\isachardoublequoteopen}op\ {\isacharequal}{\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
@@ -485,11 +485,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{typedecl}\isamarkupfalse%
 \ bar\isanewline
 \isanewline
@@ -506,29 +506,29 @@
 \isanewline
 \isacommand{end}\isamarkupfalse%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 \isanewline
 %
-\isadelimtt
+\isadelimquotett
 \isanewline
 %
-\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
@@ -539,20 +539,20 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
-\isatagtt
+\isatagquotett
 \isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
 \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
 \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
 %
-\isadelimtt
+\isadelimquotett
 %
-\endisadelimtt
+\endisadelimquotett
 %
 \isamarkupsubsection{Enhancing the target language context%
 }
@@ -565,23 +565,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 generated code.
diff -r 21b3a00a3ff0 -r 1358b1ddd915 doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Fri Oct 10 06:49:44 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Fri Oct 10 15:23:33 2008 +0200
@@ -88,11 +88,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{datatype}\isamarkupfalse%
 \ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
 \isanewline
@@ -110,43 +110,43 @@
 \ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
 \ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent Then we can generate code e.g.~for \isa{SML} as follows:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ empty\ dequeue\ enqueue\ \isakeyword{in}\ SML\isanewline
 \ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}example{\isachardot}ML{\isachardoublequoteclose}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent resulting in the following code:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -181,12 +181,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent The \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command takes a space-separated list of
@@ -201,31 +201,31 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{export{\isacharunderscore}code}\isamarkupfalse%
 \ empty\ dequeue\ enqueue\ \isakeyword{in}\ Haskell\isanewline
 \ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent This is how the corresponding code in \isa{Haskell} looks like:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -264,12 +264,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent This demonstrates the basic usage of the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command;
diff -r 21b3a00a3ff0 -r 1358b1ddd915 doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Fri Oct 10 06:49:44 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Fri Oct 10 15:23:33 2008 +0200
@@ -49,11 +49,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{lemma}\isamarkupfalse%
 \ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
@@ -63,12 +63,12 @@
 \ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
@@ -78,11 +78,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -95,12 +95,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been
@@ -117,19 +117,19 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
 \ dequeue%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent prints a table with \emph{all} defining equations
@@ -152,11 +152,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{class}\isamarkupfalse%
 \ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
 \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
@@ -210,12 +210,12 @@
 \isanewline
 \isacommand{end}\isamarkupfalse%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent We define the natural operation of the natural numbers
@@ -223,52 +223,52 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{primrec}\isamarkupfalse%
 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
 \ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent This we use to define the discrete exponentiation function:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{definition}\isamarkupfalse%
 \ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent The corresponding code:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -316,12 +316,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent This is a convenient place to show how explicit dictionary construction
@@ -329,11 +329,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -373,12 +373,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent Note the parameters with trailing underscore (\verb|A_|)
@@ -416,63 +416,63 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{lemma}\isamarkupfalse%
 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \item eliminating superfluous constants:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{lemma}\isamarkupfalse%
 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \item replacing executable but inconvenient constructs:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{lemma}\isamarkupfalse%
 \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \end{itemize}
 %
@@ -522,11 +522,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{definition}\isamarkupfalse%
 \ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline
@@ -534,12 +534,12 @@
 \isacommand{definition}\isamarkupfalse%
 \ \ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent We will use these two \qt{digits} to represent natural numbers
@@ -547,21 +547,21 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{lemma}\isamarkupfalse%
 \ {\isadigit{4}}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent Of course we also have to provide proper code equations for
@@ -569,11 +569,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{lemma}\isamarkupfalse%
 \ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
@@ -588,12 +588,12 @@
 \ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent We then instruct the code generator to view \isa{{\isadigit{0}}},
@@ -602,19 +602,19 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isadigit{0}}{\isasymColon}nat{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isasymColon}nat{\isachardoublequoteclose}\ Dig{\isadigit{0}}\ Dig{\isadigit{1}}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent For the former constructor \isa{Suc}, we provide a code
@@ -623,11 +623,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{lemma}\isamarkupfalse%
 \ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
@@ -638,23 +638,23 @@
 \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
 \isacommand{declare}\isamarkupfalse%
 \ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ del{\isacharbrackright}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent This yields the following code:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -679,12 +679,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent From this example, it can be easily glimpsed that using own constructor sets
@@ -740,11 +740,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{primrec}\isamarkupfalse%
 \ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
@@ -753,12 +753,12 @@
 \ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
 \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
 \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent The membership test during preprocessing is rewritten,
@@ -767,11 +767,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -798,12 +798,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent Obviously, polymorphic equality is implemented the Haskell
@@ -825,11 +825,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{instantiation}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}order{\isacharcomma}\ order{\isacharparenright}\ order\isanewline
 \isakeyword{begin}\isanewline
@@ -859,12 +859,12 @@
 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent Then code generation will fail.  Why?  The definition
@@ -878,11 +878,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{lemma}\isamarkupfalse%
 \ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
@@ -891,23 +891,23 @@
 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent Then code generation succeeds:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -943,12 +943,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 In some cases, the automatically derived defining equations
@@ -959,19 +959,19 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{datatype}\isamarkupfalse%
 \ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \isadelimproof
 %
@@ -1001,34 +1001,34 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{lemma}\isamarkupfalse%
 \ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
 \ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -1059,12 +1059,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \isamarkupsubsection{Explicit partiality%
 }
@@ -1076,22 +1076,22 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{fun}\isamarkupfalse%
 \ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ {\isacharbar}\ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
 \ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent In the corresponding code, there is no equation
@@ -1099,11 +1099,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -1117,12 +1117,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent In some cases it is desirable to have this
@@ -1130,11 +1130,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{axiomatization}\isamarkupfalse%
 \ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
 \isanewline
@@ -1151,12 +1151,12 @@
 \ strict{\isacharunderscore}dequeue{\isacharprime}\isanewline
 \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}q{\isacharcolon}{\isacharcolon}{\isacharprime}a\ queue{\isachardot}\ case\ q\ of\ Queue\ xs\ ys\ {\isasymRightarrow}\ length\ xs{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ simp{\isacharunderscore}all%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent For technical reasons the definition of
@@ -1175,19 +1175,19 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 \isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
 \ empty{\isacharunderscore}queue%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent Then the code generator will just insert an error or
@@ -1195,11 +1195,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
-\isatagquoteme
+\isatagquote
 %
 \begin{isamarkuptext}%
 \isaverbatim%
@@ -1214,12 +1214,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
 %
-\isadelimquoteme
+\isadelimquote
 %
-\endisadelimquoteme
+\endisadelimquote
 %
 \begin{isamarkuptext}%
 \noindent This feature however is rarely needed in practice.
diff -r 21b3a00a3ff0 -r 1358b1ddd915 doc-src/IsarAdvanced/Codegen/codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Fri Oct 10 06:49:44 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Fri Oct 10 15:23:33 2008 +0200
@@ -11,39 +11,44 @@
 \usepackage{tikz}
 \usepackage{../../pdfsetup}
 
-\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
-
-\makeatletter
-
-\isakeeptag{quoteme}
-\newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
-\renewcommand{\isatagquoteme}{\begin{quoteme}}
-\renewcommand{\endisatagquoteme}{\end{quoteme}}
+%% setup
 
-\isakeeptag{tt}
-\renewcommand{\isatagtt}{\begin{quoteme}\isabellestyle{tt}\isastyle}
-\renewcommand{\endisatagtt}{\end{quoteme}\isabellestyle{it}\isastyle}
-
-\makeatother
-
-\newcommand{\isactrlbvec}{\emph\bgroup\begin{math}{}\overline\bgroup\mbox\bgroup\isastylescript}
-\newcommand{\isactrlevec}{\egroup\egroup\end{math}\egroup}
-
-\newcommand{\qt}[1]{``#1''}
-\newcommand{\qtt}[1]{"{}{#1}"{}}
-\newcommand{\qn}[1]{\emph{#1}}
-\newcommand{\strong}[1]{{\bfseries #1}}
-\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
-
+% configuration
 \hyphenation{Isabelle}
 \hyphenation{Isar}
 
+% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+
+% verbatim text
+\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
+
+% invisibility
 \isadroptag{theory}
+
+% quoted segments
+\makeatletter
+\isakeeptag{quote}
+\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
+\renewcommand{\isatagquote}{\begin{quotesegment}}
+\renewcommand{\endisatagquote}{\end{quotesegment}}
+\makeatother
+
+\isakeeptag{quotett}
+\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
+\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}
+
+
+%% contents
+
 \title{\includegraphics[scale=0.5]{isabelle_isar}
   \\[4ex] Code generation from Isabelle/HOL theories}
 \author{\emph{Florian Haftmann}}
 
-
 \begin{document}
 
 \maketitle