--- 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.
--- 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;
--- 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.
--- 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.
--- 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;
--- 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.
--- 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