1.1 --- a/doc-src/Main/Docs/Main_Doc.thy	Sun Apr 26 20:17:50 2009 +0200
     1.2 +++ b/doc-src/Main/Docs/Main_Doc.thy	Sun Apr 26 20:18:48 2009 +0200
     1.3 @@ -268,6 +268,7 @@
     1.4  @{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
     1.5  @{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
     1.6  @{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
     1.7 +@{const compower} & @{term_type_only "op ^^ :: ('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set" "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set"}\\
     1.8  \end{tabular}
     1.9  
    1.10  \subsubsection*{Syntax}
    1.11 @@ -318,7 +319,6 @@
    1.12  @{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
    1.13  @{term "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
    1.14  @{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
    1.15 -@{term "op ^ :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
    1.16  @{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
    1.17  @{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
    1.18  @{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\
    1.19 @@ -331,7 +331,9 @@
    1.20  \end{tabular}
    1.21  
    1.22  \begin{tabular}{@ {} l @ {~::~} l @ {}}
    1.23 -@{const Nat.of_nat} & @{typeof Nat.of_nat}
    1.24 +@{const Nat.of_nat} & @{typeof Nat.of_nat}\\
    1.25 +@{term "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} &
    1.26 +  @{term_type_only "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"}
    1.27  \end{tabular}
    1.28  
    1.29  \section{Int}
    1.30 @@ -450,14 +452,6 @@
    1.31  \end{tabular}
    1.32  
    1.33  
    1.34 -\section{Iterated Functions and Relations}
    1.35 -
    1.36 -Theory: @{theory Relation_Power}
    1.37 -
    1.38 -Iterated functions \ @{term[source]"(f::'a\<Rightarrow>'a) ^ n"} \
    1.39 -and relations \ @{term[source]"(r::('a\<times>'a)set) ^ n"}.
    1.40 -
    1.41 -
    1.42  \section{Option}
    1.43  
    1.44  @{datatype option}

     2.1 --- a/doc-src/Main/Docs/document/Main_Doc.tex	Sun Apr 26 20:17:50 2009 +0200
     2.2 +++ b/doc-src/Main/Docs/document/Main_Doc.tex	Sun Apr 26 20:18:48 2009 +0200
     2.3 @@ -279,6 +279,7 @@
     2.4  \isa{rtrancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
     2.5  \isa{trancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
     2.6  \isa{reflcl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
     2.7 +\isa{op\ {\isacharcircum}{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
     2.8  \end{tabular}
     2.9  
    2.10  \subsubsection*{Syntax}
    2.11 @@ -328,7 +329,6 @@
    2.12  \isa{op\ {\isacharplus}} &
    2.13  \isa{op\ {\isacharminus}} &
    2.14  \isa{op\ {\isacharasterisk}} &
    2.15 -\isa{op\ {\isacharcircum}} &
    2.16  \isa{op\ div}&
    2.17  \isa{op\ mod}&
    2.18  \isa{op\ dvd}\\
    2.19 @@ -341,7 +341,9 @@
    2.20  \end{tabular}
    2.21  
    2.22  \begin{tabular}{@ {} l @ {~::~} l @ {}}
    2.23 -\isa{of{\isacharunderscore}nat} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a}
    2.24 +\isa{of{\isacharunderscore}nat} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a}\\
    2.25 +\isa{op\ {\isacharcircum}{\isacharcircum}} &
    2.26 +  \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}
    2.27  \end{tabular}
    2.28  
    2.29  \section{Int}
    2.30 @@ -460,14 +462,6 @@
    2.31  \end{tabular}
    2.32  
    2.33  
    2.34 -\section{Iterated Functions and Relations}
    2.35 -
    2.36 -Theory: \isa{Relation{\isacharunderscore}Power}
    2.37 -
    2.38 -Iterated functions \ \isa{{\isachardoublequote}{\isacharparenleft}f{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isasymRightarrow}{\isacharprime}a{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}} \
    2.39 -and relations \ \isa{{\isachardoublequote}{\isacharparenleft}r{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}a{\isacharparenright}set{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}}.
    2.40 -
    2.41 -
    2.42  \section{Option}
    2.43  
    2.44  \isa{\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a}

     3.1 --- a/src/HOL/Wellfounded.thy	Sun Apr 26 20:17:50 2009 +0200
     3.2 +++ b/src/HOL/Wellfounded.thy	Sun Apr 26 20:18:48 2009 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  header {*Well-founded Recursion*}
     3.5  
     3.6  theory Wellfounded
     3.7 -imports Finite_Set Transitive_Closure Nat
     3.8 +imports Finite_Set Wellfounded Nat
     3.9  uses ("Tools/function_package/size.ML")
    3.10  begin
    3.11