doc-src/Codegen/Thy/document/Further.tex
changeset 39440 985b13c5a61d
parent 39304 352bcd845998
child 39802 e7d4923b9b1c
     1.1 --- a/doc-src/Codegen/Thy/document/Further.tex	Tue Sep 07 16:49:32 2010 +0200
     1.2 +++ b/doc-src/Codegen/Thy/document/Further.tex	Tue Sep 07 16:58:01 2010 +0200
     1.3 @@ -216,13 +216,13 @@
     1.4  \begin{isamarkuptext}%
     1.5  \isatypewriter%
     1.6  \noindent%
     1.7 -\hspace*{0pt}funpow ::~forall a.~Example.Nat -> (a -> a) -> a -> a;\\
     1.8 -\hspace*{0pt}funpow Example.Zero{\char95}nat f = id;\\
     1.9 -\hspace*{0pt}funpow (Example.Suc n) f = f .~Example.funpow n f;\\
    1.10 +\hspace*{0pt}funpow ::~forall a.~Nat -> (a -> a) -> a -> a;\\
    1.11 +\hspace*{0pt}funpow Zero{\char95}nat f = id;\\
    1.12 +\hspace*{0pt}funpow (Suc n) f = f .~funpow n f;\\
    1.13  \hspace*{0pt}\\
    1.14 -\hspace*{0pt}funpows ::~forall a.~[Example.Nat] -> (a -> a) -> a -> a;\\
    1.15 +\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
    1.16  \hspace*{0pt}funpows [] = id;\\
    1.17 -\hspace*{0pt}funpows (x :~xs) = Example.funpow x .~Example.funpows xs;%
    1.18 +\hspace*{0pt}funpows (x :~xs) = funpow x .~funpows xs;%
    1.19  \end{isamarkuptext}%
    1.20  \isamarkuptrue%
    1.21  %