# HG changeset patch
# User haftmann
# Date 1240727693 -7200
# Node ID b53800e3ee47bbc59966b41a15fc207ccee8bdba
# Parent  2bbc22bd6a9519da5faf98bba0958247dded566f
adjusted to changes in power syntax

diff -r 2bbc22bd6a95 -r b53800e3ee47 doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Sun Apr 26 00:42:59 2009 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Sun Apr 26 08:34:53 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}
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}
diff -r 2bbc22bd6a95 -r b53800e3ee47 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sun Apr 26 00:42:59 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Sun Apr 26 08:34:53 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