doc-src/Codegen/Thy/document/Further.tex
changeset 39210 985b13c5a61d
parent 39070 352bcd845998
child 39559 e7d4923b9b1c
--- a/doc-src/Codegen/Thy/document/Further.tex	Tue Sep 07 16:49:32 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex	Tue Sep 07 16:58:01 2010 +0200
@@ -216,13 +216,13 @@
 \begin{isamarkuptext}%
 \isatypewriter%
 \noindent%
-\hspace*{0pt}funpow ::~forall a.~Example.Nat -> (a -> a) -> a -> a;\\
-\hspace*{0pt}funpow Example.Zero{\char95}nat f = id;\\
-\hspace*{0pt}funpow (Example.Suc n) f = f .~Example.funpow n f;\\
+\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
+\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
+\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
 \hspace*{0pt}\\
-\hspace*{0pt}funpows ::~forall a.~[Example.Nat] -> (a -> a) -> a -> a;\\
+\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
 \hspace*{0pt}funpows [] = id;\\
-\hspace*{0pt}funpows (x :~xs) = Example.funpow x .~Example.funpows xs;%
+\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %