--- a/doc-src/Main/Docs/Main_Doc.thy Sun Apr 26 20:17:50 2009 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy Sun Apr 26 20:18:48 2009 +0200
@@ -268,6 +268,7 @@
@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
+@{const compower} & @{term_type_only "op ^^ :: ('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set" "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set"}\\
\end{tabular}
\subsubsection*{Syntax}
@@ -318,7 +319,6 @@
@{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
@{term "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
@{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
-@{term "op ^ :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
@{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
@{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
@{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\
@@ -331,7 +331,9 @@
\end{tabular}
\begin{tabular}{@ {} l @ {~::~} l @ {}}
-@{const Nat.of_nat} & @{typeof Nat.of_nat}
+@{const Nat.of_nat} & @{typeof Nat.of_nat}\\
+@{term "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} &
+ @{term_type_only "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"}
\end{tabular}
\section{Int}
@@ -450,14 +452,6 @@
\end{tabular}
-\section{Iterated Functions and Relations}
-
-Theory: @{theory Relation_Power}
-
-Iterated functions \ @{term[source]"(f::'a\<Rightarrow>'a) ^ n"} \
-and relations \ @{term[source]"(r::('a\<times>'a)set) ^ n"}.
-
-
\section{Option}
@{datatype option}
--- a/doc-src/Main/Docs/document/Main_Doc.tex Sun Apr 26 20:17:50 2009 +0200
+++ b/doc-src/Main/Docs/document/Main_Doc.tex Sun Apr 26 20:18:48 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}
--- a/src/HOL/Wellfounded.thy Sun Apr 26 20:17:50 2009 +0200
+++ b/src/HOL/Wellfounded.thy Sun Apr 26 20:18:48 2009 +0200
@@ -7,7 +7,7 @@
header {*Well-founded Recursion*}
theory Wellfounded
-imports Finite_Set Transitive_Closure Nat
+imports Finite_Set Wellfounded Nat
uses ("Tools/function_package/size.ML")
begin