| author | wenzelm |
| Thu, 16 Mar 2000 00:35:27 +0100 | |
| changeset 8490 | 6e0f23304061 |
| parent 5780 | 0187f936685a |
| child 8844 | db71c334e854 |
| 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 |
||
|
5780
0187f936685a
Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
paulson
parents:
5608
diff
changeset
|
11 |
instance |
|
0187f936685a
Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
paulson
parents:
5608
diff
changeset
|
12 |
set :: (term) {power} (* only ('a * 'a) set should be in power! *)
|
|
0187f936685a
Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
paulson
parents:
5608
diff
changeset
|
13 |
|
| 5183 | 14 |
primrec |
| 5608 | 15 |
"R^0 = Id" |
| 2740 | 16 |
"R^(Suc n) = R O (R^n)" |
17 |
||
| 1496 | 18 |
end |