changeset 10213 | 01c2744a3786 |
child 11305 | 2ce86fccc95b |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Relation_Power.thy Thu Oct 12 18:44:35 2000 +0200 @@ -0,0 +1,18 @@ +(* Title: HOL/Relation_Power.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 1996 TU Muenchen + +R^n = R O ... O R, the n-fold composition of R +*) + +Relation_Power = 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