# HG changeset patch
# User haftmann
# Date 1222945653 -7200
# Node ID 7a558c87210470d300cf210ae728dc66ebaecb96
# Parent  a79701b14a302b228cf9261851159da65035b06c
tuned

diff -r a79701b14a30 -r 7a558c872104 doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy
--- 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:
 *}
 
diff -r a79701b14a30 -r 7a558c872104 doc-src/IsarAdvanced/Codegen/Thy/Program.thy
--- 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
diff -r a79701b14a30 -r 7a558c872104 doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
--- 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%
diff -r a79701b14a30 -r 7a558c872104 doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex
--- 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%
 %