| author | wenzelm |
| Fri, 25 Apr 1997 17:50:55 +0200 | |
| changeset 3061 | 25b2a895f864 |
| parent 2740 | 2c549ae2563b |
| child 3370 | 5c5fdce3a4e4 |
| 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)
|
|
| 2740 | 13 |
|
14 |
primrec "op ^" nat |
|
15 |
"R^0 = id" |
|
16 |
"R^(Suc n) = R O (R^n)" |
|
17 |
||
| 1496 | 18 |
end |