--- a/doc-src/Codegen/Thy/Adaptation.thy Fri Sep 24 14:57:17 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Fri Sep 24 15:14:55 2010 +0200
@@ -175,10 +175,8 @@
code_const %invisible True and False and "op \<and>" and Not
(SML and and and)
(*>*)
-text %quote {*
- \begin{typewriter}
- @{code_stmts in_interval (SML)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts in_interval (SML)}
*}
text {*
@@ -208,10 +206,8 @@
placeholder for the type constructor's (the constant's) arguments.
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts in_interval (SML)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts in_interval (SML)}
*}
text {*
@@ -225,10 +221,8 @@
code_const %quotett "op \<and>"
(SML infixl 1 "andalso")
-text %quote {*
- \begin{typewriter}
- @{code_stmts in_interval (SML)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts in_interval (SML)}
*}
text {*
--- a/doc-src/Codegen/Thy/Foundations.thy Fri Sep 24 14:57:17 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Fri Sep 24 15:14:55 2010 +0200
@@ -161,10 +161,8 @@
is determined syntactically. The resulting code:
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts dequeue (consts) dequeue (Haskell)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts dequeue (consts) dequeue (Haskell)}
*}
text {*
@@ -219,10 +217,8 @@
equality check, as can be seen in the corresponding @{text SML} code:
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts collect_duplicates (SML)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts collect_duplicates (SML)}
*}
text {*
@@ -259,10 +255,8 @@
for the pattern @{term "AQueue [] []"}:
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
*}
text {*
@@ -302,10 +296,8 @@
exception at the appropriate position:
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
*}
text {*
--- a/doc-src/Codegen/Thy/Further.thy Fri Sep 24 14:57:17 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Fri Sep 24 15:14:55 2010 +0200
@@ -112,10 +112,8 @@
After this setup procedure, code generation can continue as usual:
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
*}
--- a/doc-src/Codegen/Thy/Inductive_Predicate.thy Fri Sep 24 14:57:17 2010 +0200
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Fri Sep 24 15:14:55 2010 +0200
@@ -113,8 +113,8 @@
*}
text %quote {*
- @{thm tranclp.intros(1)[of r a b]} \\
- @{thm tranclp.intros(2)[of r a b c]}
+ @{lemma [source] "r a b \<Longrightarrow> tranclp r a b" by (fact tranclp.intros(1))}\\
+ @{lemma [source] "tranclp r a b \<Longrightarrow> r b c \<Longrightarrow> tranclp r a c" by (fact tranclp.intros(2))}
*}
text {*
@@ -127,8 +127,8 @@
*}
lemma %quote [code_pred_intro]:
- "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ a b"
- "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
+ "r a b \<Longrightarrow> tranclp r a b"
+ "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
by auto
text {*
@@ -142,7 +142,7 @@
code_pred %quote tranclp
proof -
case tranclp
- from this converse_tranclpE [OF this(1)] show thesis by metis
+ from this converse_tranclpE [OF tranclp.prems] show thesis by metis
qed
text {*
@@ -152,7 +152,7 @@
*}
text %quote {*
- @{thm [display] lexord_def[of "r"]}
+ @{thm [display] lexord_def [of r]}
*}
text {*
@@ -260,7 +260,7 @@
text {*
Further examples for compiling inductive predicates can be found in
- the @{text "HOL/ex/Predicate_Compile_ex,thy"} theory file. There are
+ the @{text "HOL/ex/Predicate_Compile_ex.thy"} theory file. There are
also some examples in the Archive of Formal Proofs, notably in the
@{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
sessions.
--- a/doc-src/Codegen/Thy/Introduction.thy Fri Sep 24 14:57:17 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Fri Sep 24 15:14:55 2010 +0200
@@ -70,10 +70,8 @@
text {* \noindent resulting in the following code: *}
-text %quote {*
- \begin{typewriter}
- @{code_stmts empty enqueue dequeue (SML)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts empty enqueue dequeue (SML)}
*}
text {*
@@ -95,10 +93,8 @@
\noindent This is the corresponding code:
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts empty enqueue dequeue (Haskell)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts empty enqueue dequeue (Haskell)}
*}
text {*
@@ -172,10 +168,8 @@
native classes:
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts bexp (Haskell)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts bexp (Haskell)}
*}
text {*
@@ -184,10 +178,8 @@
@{text SML}:
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts bexp (SML)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts bexp (SML)}
*}
text {*
--- a/doc-src/Codegen/Thy/Refinement.thy Fri Sep 24 14:57:17 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy Fri Sep 24 15:14:55 2010 +0200
@@ -31,10 +31,8 @@
to two recursive calls:
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts fib (consts) fib (Haskell)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts fib (consts) fib (Haskell)}
*}
text {*
@@ -71,10 +69,8 @@
\noindent The resulting code shows only linear growth of runtime:
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts fib (consts) fib fib_step (Haskell)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts fib (consts) fib fib_step (Haskell)}
*}
@@ -161,10 +157,8 @@
\noindent The resulting code looks as expected:
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts empty enqueue dequeue (SML)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts empty enqueue dequeue (SML)}
*}
text {*
@@ -259,10 +253,8 @@
\noindent Then the corresponding code is as follows:
*}
-text %quote {*
- \begin{typewriter}
- @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
- \end{typewriter}
+text %quote %typewriter {*
+ @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
*} (*(types) dlist (consts) dempty dinsert dremove list_of List.member insert remove *)
text {*
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Fri Sep 24 14:57:17 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Fri Sep 24 15:14:55 2010 +0200
@@ -228,15 +228,14 @@
%
\endisadeliminvisible
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- structure\ Example\ {\isacharcolon}\ sig\isanewline
+structure\ Example\ {\isacharcolon}\ sig\isanewline
\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
\ \ datatype\ boola\ {\isacharequal}\ True\ {\isacharbar}\ False\isanewline
\ \ val\ conj\ {\isacharcolon}\ boola\ {\isacharminus}{\isachargreater}\ boola\ {\isacharminus}{\isachargreater}\ boola\isanewline
@@ -261,18 +260,16 @@
\isanewline
fun\ in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isacharequal}\ conj\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ k\ n{\isacharparenright}\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ n\ l{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
-end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
-
- \end{typewriter}%
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
\noindent Though this is correct code, it is a little bit
@@ -314,15 +311,14 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- structure\ Example\ {\isacharcolon}\ sig\isanewline
+structure\ Example\ {\isacharcolon}\ sig\isanewline
\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
\ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
\ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
@@ -338,18 +334,16 @@
\isanewline
fun\ in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ k\ n{\isacharparenright}\ andalso\ {\isacharparenleft}less{\isacharunderscore}eq{\isacharunderscore}nat\ n\ l{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
-end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
-
- \end{typewriter}%
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
\noindent This still is not perfect: the parentheses around the
@@ -375,15 +369,14 @@
%
\endisadelimquotett
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- structure\ Example\ {\isacharcolon}\ sig\isanewline
+structure\ Example\ {\isacharcolon}\ sig\isanewline
\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
\ \ val\ less{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
\ \ val\ less{\isacharunderscore}eq{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ bool\isanewline
@@ -399,18 +392,16 @@
\isanewline
fun\ in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isacharequal}\ less{\isacharunderscore}eq{\isacharunderscore}nat\ k\ n\ andalso\ less{\isacharunderscore}eq{\isacharunderscore}nat\ n\ l{\isacharsemicolon}\isanewline
\isanewline
-end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
-
- \end{typewriter}%
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
\noindent The attentive reader may ask how we assert that no
--- a/doc-src/Codegen/Thy/document/Foundations.tex Fri Sep 24 14:57:17 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Fri Sep 24 15:14:55 2010 +0200
@@ -238,29 +238,27 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
+dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Just\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ {\isacharparenleft}if\ null\ xs\ then\ {\isacharparenleft}Nothing{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
-\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}
- \end{typewriter}%
+\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has
@@ -269,7 +267,7 @@
This possibility to select arbitrary code equations is the key
technique for program and datatype refinement (see
- \secref{sec:refinement}.
+ \secref{sec:refinement}).
Due to the preprocessor, there is the distinction of raw code
equations (before preprocessing) and code equations (after
@@ -340,15 +338,14 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- structure\ Example\ {\isacharcolon}\ sig\isanewline
+structure\ Example\ {\isacharcolon}\ sig\isanewline
\ \ type\ {\isacharprime}a\ equal\isanewline
\ \ val\ equal\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline
\ \ val\ eq\ {\isacharcolon}\ {\isacharprime}a\ equal\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ bool\isanewline
@@ -372,18 +369,16 @@
\ \ \ \ \ \ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ xs\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}\ zs{\isacharparenright}\isanewline
\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ A{\isacharunderscore}\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ xs{\isacharparenright}\ {\isacharparenleft}z\ {\isacharcolon}{\isacharcolon}\ ys{\isacharparenright}\ zs{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
-end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
-
- \end{typewriter}%
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
\noindent Obviously, polymorphic equality is implemented the Haskell
@@ -436,30 +431,28 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
+strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ let\ {\isacharbraceleft}\isanewline
\ \ \ \ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}\ {\isacharequal}\ reverse\ xs{\isacharsemicolon}\isanewline
\ \ {\isacharbraceright}\ in\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
-strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}
- \end{typewriter}%
+strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
\noindent In some cases it is desirable to have this
@@ -527,32 +520,30 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a{\isacharsemicolon}\isanewline
+empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a{\isacharsemicolon}\isanewline
empty{\isacharunderscore}queue\ {\isacharequal}\ error\ {\isachardoublequote}empty{\isacharunderscore}queue{\isachardoublequote}{\isacharsemicolon}\isanewline
\isanewline
strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharcolon}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ {\isacharparenleft}if\ null\ xs\ then\ empty{\isacharunderscore}queue\isanewline
-\ \ \ \ else\ strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}
- \end{typewriter}%
+\ \ \ \ else\ strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}reverse\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
\noindent This feature however is rarely needed in practice. Note
--- a/doc-src/Codegen/Thy/document/Further.tex Fri Sep 24 14:57:17 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Fri Sep 24 15:14:55 2010 +0200
@@ -207,31 +207,29 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- funpow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
+funpow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
funpow\ Zero{\isacharunderscore}nat\ f\ {\isacharequal}\ id{\isacharsemicolon}\isanewline
funpow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ f\ {\isacharequal}\ f\ {\isachardot}\ funpow\ n\ f{\isacharsemicolon}\isanewline
\isanewline
funpows\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharbrackleft}Nat{\isacharbrackright}\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
funpows\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ id{\isacharsemicolon}\isanewline
-funpows\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ funpow\ x\ {\isachardot}\ funpows\ xs{\isacharsemicolon}
- \end{typewriter}%
+funpows\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ {\isacharequal}\ funpow\ x\ {\isachardot}\ funpows\ xs{\isacharsemicolon}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\isamarkupsubsection{Imperative data structures%
}
--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Fri Sep 24 14:57:17 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Fri Sep 24 15:14:55 2010 +0200
@@ -245,8 +245,8 @@
\isatagquote
%
\begin{isamarkuptext}%
-\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b} \\
- \isa{r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b\ {\isasymLongrightarrow}\ r\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}%
+\isa{{\isachardoublequote}r\ a\ b\ {\isasymLongrightarrow}\ tranclp\ r\ a\ b{\isachardoublequote}}\\
+ \isa{{\isachardoublequote}tranclp\ r\ a\ b\ {\isasymLongrightarrow}\ r\ b\ c\ {\isasymLongrightarrow}\ tranclp\ r\ a\ c{\isachardoublequote}}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -273,8 +273,8 @@
\isatagquote
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ tranclp\ r\ a\ b{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ tranclp\ r\ b\ c\ {\isasymLongrightarrow}\ tranclp\ r\ a\ c{\isachardoublequoteclose}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagquote
@@ -305,7 +305,7 @@
\ \ \isacommand{case}\isamarkupfalse%
\ tranclp\isanewline
\ \ \isacommand{from}\isamarkupfalse%
-\ this\ converse{\isacharunderscore}tranclpE\ {\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
+\ this\ converse{\isacharunderscore}tranclpE\ {\isacharbrackleft}OF\ tranclp{\isachardot}prems{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
\ thesis\ \isacommand{by}\isamarkupfalse%
\ metis\isanewline
\isacommand{qed}\isamarkupfalse%
@@ -471,7 +471,7 @@
%
\begin{isamarkuptext}%
Further examples for compiling inductive predicates can be found in
- the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex{\isacharcomma}thy} theory file. There are
+ the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex{\isachardot}thy} theory file. There are
also some examples in the Archive of Formal Proofs, notably in the
\isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava}
sessions.%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Fri Sep 24 14:57:17 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Fri Sep 24 15:14:55 2010 +0200
@@ -133,15 +133,14 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- structure\ Example\ {\isacharcolon}\ sig\isanewline
+structure\ Example\ {\isacharcolon}\ sig\isanewline
\ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
\ \ val\ fold\ {\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b{\isacharparenright}\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\isanewline
\ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline
@@ -173,18 +172,16 @@
\isanewline
fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
-end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
-
- \end{typewriter}%
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
\noindent The \indexdef{}{command}{export\_code}\hypertarget{command.export-code}{\hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}} command takes a
@@ -219,15 +216,14 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- module\ Example\ where\ {\isacharbraceleft}\isanewline
+module\ Example\ where\ {\isacharbraceleft}\isanewline
\isanewline
data\ Queue\ a\ {\isacharequal}\ AQueue\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline
\isanewline
@@ -245,18 +241,16 @@
enqueue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a\ {\isacharminus}{\isachargreater}\ Queue\ a\ {\isacharminus}{\isachargreater}\ Queue\ a{\isacharsemicolon}\isanewline
enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}\ xs{\isacharparenright}\ ys{\isacharsemicolon}\isanewline
\isanewline
-{\isacharbraceright}\isanewline
-
- \end{typewriter}%
+{\isacharbraceright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
\noindent For more details about \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} see
@@ -388,15 +382,14 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- module\ Example\ where\ {\isacharbraceleft}\isanewline
+module\ Example\ where\ {\isacharbraceleft}\isanewline
\isanewline
data\ Nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ Nat{\isacharsemicolon}\isanewline
\isanewline
@@ -434,18 +427,16 @@
bexp\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
-{\isacharbraceright}\isanewline
-
- \end{typewriter}%
+{\isacharbraceright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
\noindent This is a convenient place to show how explicit dictionary
@@ -454,15 +445,14 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- structure\ Example\ {\isacharcolon}\ sig\isanewline
+structure\ Example\ {\isacharcolon}\ sig\isanewline
\ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
\ \ val\ plus{\isacharunderscore}nat\ {\isacharcolon}\ nat\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
\ \ type\ {\isacharprime}a\ semigroup\isanewline
@@ -505,18 +495,16 @@
\isanewline
fun\ bexp\ n\ {\isacharequal}\ pow\ monoid{\isacharunderscore}nat\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
-end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
-
- \end{typewriter}%
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
\noindent Note the parameters with trailing underscore (\verb|A_|), which are the dictionary parameters.%
--- a/doc-src/Codegen/Thy/document/Refinement.tex Fri Sep 24 14:57:17 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Fri Sep 24 15:14:55 2010 +0200
@@ -65,28 +65,26 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
+fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
fib\ {\isacharparenleft}Suc\ Zero{\isacharunderscore}nat{\isacharparenright}\ {\isacharequal}\ Suc\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline
-fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ plus{\isacharunderscore}nat\ {\isacharparenleft}fib\ n{\isacharparenright}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon}
- \end{typewriter}%
+fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ plus{\isacharunderscore}nat\ {\isacharparenleft}fib\ n{\isacharparenright}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
\noindent A more efficient implementation would use dynamic
@@ -163,15 +161,14 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline
+fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline
fib{\isacharunderscore}step\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ let\ {\isacharbraceleft}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}m{\isacharcomma}\ q{\isacharparenright}\ {\isacharequal}\ fib{\isacharunderscore}step\ n{\isacharsemicolon}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbraceright}\ in\ {\isacharparenleft}plus{\isacharunderscore}nat\ m\ q{\isacharcomma}\ m{\isacharparenright}{\isacharsemicolon}\isanewline
@@ -179,17 +176,16 @@
\isanewline
fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
fib\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fst\ {\isacharparenleft}fib{\isacharunderscore}step\ n{\isacharparenright}{\isacharsemicolon}\isanewline
-fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}
- \end{typewriter}%
+fib\ Zero{\isacharunderscore}nat\ {\isacharequal}\ Zero{\isacharunderscore}nat{\isacharsemicolon}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\isamarkupsubsection{Datatype refinement%
}
@@ -341,15 +337,14 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- structure\ Example\ {\isacharcolon}\ sig\isanewline
+structure\ Example\ {\isacharcolon}\ sig\isanewline
\ \ val\ id\ {\isacharcolon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\isanewline
\ \ val\ fold\ {\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b{\isacharparenright}\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\isanewline
\ \ val\ rev\ {\isacharcolon}\ {\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ list\isanewline
@@ -381,18 +376,16 @@
\isanewline
fun\ enqueue\ x\ {\isacharparenleft}AQueue\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ xs{\isacharcomma}\ ys{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
-end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
-
- \end{typewriter}%
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
The same techniques can also be applied to types which are not
@@ -578,15 +571,14 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
-\isatagquote
+\isatagtypewriter
%
\begin{isamarkuptext}%
-\begin{typewriter}
- module\ Example\ where\ {\isacharbraceleft}\isanewline
+module\ Example\ where\ {\isacharbraceleft}\isanewline
\isanewline
newtype\ Dlist\ a\ {\isacharequal}\ Dlist\ {\isacharbrackleft}a{\isacharbrackright}{\isacharsemicolon}\isanewline
\isanewline
@@ -613,18 +605,16 @@
remove\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ {\isacharparenleft}Eq\ a{\isacharparenright}\ {\isacharequal}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a\ {\isacharminus}{\isachargreater}\ Dlist\ a{\isacharsemicolon}\isanewline
remove\ x\ dxs\ {\isacharequal}\ Dlist\ {\isacharparenleft}remove{\isadigit{1}}\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
\isanewline
-{\isacharbraceright}\isanewline
-
- \end{typewriter}%
+{\isacharbraceright}\isanewline%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
%
-\isadelimquote
+\isadelimtypewriter
%
-\endisadelimquote
+\endisadelimtypewriter
%
\begin{isamarkuptext}%
Typical data structures implemented by representations involving