# 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\('a*'a)set"}\\ @{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\('a*'a)set"}\\ @{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\('a*'a)set"}\\ +@{const compower} & @{term_type_only "op ^^ :: ('a*'a)set\nat\('a*'a)set" "('a*'a)set\nat\('a*'a)set"}\\ \end{tabular} \subsubsection*{Syntax} @@ -318,7 +319,6 @@ @{term "op + :: nat \ nat \ nat"} & @{term "op - :: nat \ nat \ nat"} & @{term "op * :: nat \ nat \ nat"} & -@{term "op ^ :: nat \ nat \ nat"} & @{term "op div :: nat \ nat \ nat"}& @{term "op mod :: nat \ nat \ nat"}& @{term "op dvd :: nat \ nat \ 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 \ 'a) \ nat \ 'a \ 'a"} & + @{term_type_only "op ^^ :: ('a \ 'a) \ nat \ 'a \ 'a" "('a \ 'a) \ nat \ 'a \ '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\'a) ^ n"} \ -and relations \ @{term[source]"(r::('a\'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