doc-src/Codegen/Thy/document/Foundations.tex
changeset 39210 985b13c5a61d
parent 39070 352bcd845998
child 39664 0afaf89ab591
--- a/doc-src/Codegen/Thy/document/Foundations.tex	Tue Sep 07 16:49:32 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex	Tue Sep 07 16:58:01 2010 +0200
@@ -247,11 +247,11 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}dequeue ::~forall a.~Example.Queue a -> (Maybe a,~Example.Queue a);\\
-\hspace*{0pt}dequeue (Example.AQueue xs (y :~ys)) = (Just y,~Example.AQueue xs ys);\\
-\hspace*{0pt}dequeue (Example.AQueue xs []) =\\
-\hspace*{0pt} ~(if null xs then (Nothing,~Example.AQueue [] [])\\
-\hspace*{0pt} ~~~else Example.dequeue (Example.AQueue [] (reverse xs)));%
+\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
+\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
+\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -444,12 +444,12 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\
+\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
 \hspace*{0pt} ~let {\char123}\\
 \hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
-\hspace*{0pt} ~{\char125}~in (y,~Example.AQueue [] ys);\\
-\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);%
+\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -538,11 +538,11 @@
 \hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
 \hspace*{0pt}\\
-\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Example.Queue a -> (a,~Example.Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs (y :~ys)) = (y,~Example.AQueue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue (Example.AQueue xs []) =\\
-\hspace*{0pt} ~(if null xs then Example.empty{\char95}queue\\
-\hspace*{0pt} ~~~else Example.strict{\char95}dequeue (Example.AQueue [] (reverse xs)));%
+\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
+\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %