--- a/doc-src/Codegen/Thy/document/Further.tex Mon Jun 14 16:00:47 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Tue Jun 15 07:41:37 2010 +0200
@@ -36,27 +36,6 @@
\isamarkupsubsection{Locales and interpretation%
}
\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ funpow{\isacharunderscore}mult{\isacharcolon}\ %
-\isamarkupcmt{FIXME%
-}
-\isanewline
-\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}f\ {\isacharcircum}{\isacharcircum}\ m{\isacharparenright}\ {\isacharcircum}{\isacharcircum}\ n\ {\isacharequal}\ f\ {\isacharcircum}{\isacharcircum}\ {\isacharparenleft}m\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-\ \ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ n{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ funpow{\isacharunderscore}add{\isacharparenright}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
%
\begin{isamarkuptext}%
A technical issue comes to surface when generating code from
@@ -202,8 +181,8 @@
\isatypewriter%
\noindent%
\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}funpow Zero{\char95}nat f = id;\\
\hspace*{0pt}\\
\hspace*{0pt}funpows ::~forall a.~[Nat] -> (a -> a) -> a -> a;\\
\hspace*{0pt}funpows [] = id;\\