author | clasohm |
Fri, 08 Mar 1996 13:11:09 +0100 | |
changeset 1558 | 9c6ebfab4e05 |
parent 1496 | c443b2adaf52 |
child 1824 | 44254696843a |
permissions | -rw-r--r-- |
1496 | 1 |
(* Title: HOL/RelPow.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1996 TU Muenchen |
|
5 |
||
6 |
R^n = R O ... O R, the n-fold composition of R |
|
7 |
*) |
|
8 |
||
9 |
RelPow = Nat + |
|
10 |
||
11 |
consts |
|
12 |
"^" :: "('a * 'a) set => nat => ('a * 'a) set" (infixr 100) |
|
13 |
defs |
|
14 |
rel_pow_def "R^n == nat_rec n id (%m S. R O S)" |
|
15 |
end |