changeset 10213 | 01c2744a3786 |
parent 10212 | 33fe2d701ddd |
child 10214 | 77349ed89f45 |
--- a/src/HOL/RelPow.thy Thu Oct 12 18:38:23 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* Title: HOL/RelPow.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1996 TU Muenchen - -R^n = R O ... O R, the n-fold composition of R -*) - -RelPow = Nat + - -instance - set :: (term) {power} (* only ('a * 'a) set should be in power! *) - -primrec (relpow) - "R^0 = Id" - "R^(Suc n) = R O (R^n)" - -end