--- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Thu Oct 02 12:17:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Thu Oct 02 13:07:33 2008 +0200
@@ -60,7 +60,7 @@
*}
text {*
- Consider the following function and its corresponding
+ \noindent Consider the following function and its corresponding
SML code:
*}
--- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Thu Oct 02 12:17:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Thu Oct 02 13:07:33 2008 +0200
@@ -27,7 +27,8 @@
lemma %quoteme [code func]:
"dequeue (Queue xs []) =
- (if xs = [] then (None, Queue [] []) else dequeue (Queue [] (rev xs)))"
+ (if xs = [] then (None, Queue [] [])
+ else dequeue (Queue [] (rev xs)))"
"dequeue (Queue xs (y # ys)) =
(Some y, Queue xs ys)"
by (cases xs, simp_all) (cases "rev xs", simp_all)
@@ -39,7 +40,7 @@
the corresponding constant is determined syntactically. The resulting code:
*}
-text %quoteme {*@{code_stmts empty enqueue dequeue (Haskell)}*}
+text %quoteme {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
text {*
\noindent You may note that the equality test @{term "xs = []"} has been
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Thu Oct 02 12:17:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Thu Oct 02 13:07:33 2008 +0200
@@ -83,7 +83,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Consider the following function and its corresponding
+\noindent Consider the following function and its corresponding
SML code:%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Thu Oct 02 12:17:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Thu Oct 02 13:07:33 2008 +0200
@@ -57,7 +57,8 @@
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
@@ -86,35 +87,11 @@
\begin{isamarkuptext}%
\isaverbatim%
\noindent%
-\verb|module Example where {|\newline%
-\newline%
-\newline%
-\verb|foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;|\newline%
-\verb|foldla f a [] = a;|\newline%
-\verb|foldla f a (x : xs) = foldla f (f a x) xs;|\newline%
-\newline%
-\verb|rev :: forall a. [a] -> [a];|\newline%
-\verb|rev xs = foldla (\ xsa x -> x : xsa) [] xs;|\newline%
-\newline%
-\verb|nulla :: forall a. [a] -> Bool;|\newline%
-\verb|nulla (x : xs) = False;|\newline%
-\verb|nulla [] = True;|\newline%
-\newline%
-\verb|data Queue a = Queue [a] [a];|\newline%
-\newline%
-\verb|empty :: forall a. Queue a;|\newline%
-\verb|empty = Queue [] [];|\newline%
-\newline%
\verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline%
\verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline%
\verb|dequeue (Queue xs []) =|\newline%
\verb| (if nulla xs then (Nothing, Queue [] [])|\newline%
-\verb| else dequeue (Queue [] (rev xs)));|\newline%
-\newline%
-\verb|enqueue :: forall a. a -> Queue a -> Queue a;|\newline%
-\verb|enqueue x (Queue xs ys) = Queue (x : xs) ys;|\newline%
-\newline%
-\verb|}|%
+\verb| else dequeue (Queue [] (rev xs)));|%
\end{isamarkuptext}%
\isamarkuptrue%
%