diff -r 2bbc22bd6a95 -r b53800e3ee47 doc-src/Main/Docs/document/Main_Doc.tex
--- a/doc-src/Main/Docs/document/Main_Doc.tex	Sun Apr 26 00:42:59 2009 +0200
+++ b/doc-src/Main/Docs/document/Main_Doc.tex	Sun Apr 26 08:34:53 2009 +0200
@@ -279,6 +279,7 @@
 \isa{rtrancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
 \isa{trancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
 \isa{reflcl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
+\isa{op\ {\isacharcircum}{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
 \end{tabular}
 
 \subsubsection*{Syntax}
@@ -328,7 +329,6 @@
 \isa{op\ {\isacharplus}} &
 \isa{op\ {\isacharminus}} &
 \isa{op\ {\isacharasterisk}} &
-\isa{op\ {\isacharcircum}} &
 \isa{op\ div}&
 \isa{op\ mod}&
 \isa{op\ dvd}\\
@@ -341,7 +341,9 @@
 \end{tabular}
 
 \begin{tabular}{@ {} l @ {~::~} l @ {}}
-\isa{of{\isacharunderscore}nat} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a}
+\isa{of{\isacharunderscore}nat} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a}\\
+\isa{op\ {\isacharcircum}{\isacharcircum}} &
+  \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}
 \end{tabular}
 
 \section{Int}
@@ -460,14 +462,6 @@
 \end{tabular}
 
 
-\section{Iterated Functions and Relations}
-
-Theory: \isa{Relation{\isacharunderscore}Power}
-
-Iterated functions \ \isa{{\isachardoublequote}{\isacharparenleft}f{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isasymRightarrow}{\isacharprime}a{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}} \
-and relations \ \isa{{\isachardoublequote}{\isacharparenleft}r{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}a{\isacharparenright}set{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}}.
-
-
 \section{Option}
 
 \isa{\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a}