| changeset 2740 | 2c549ae2563b |
| parent 1824 | 44254696843a |
| child 3370 | 5c5fdce3a4e4 |
--- a/src/HOL/RelPow.thy Thu Mar 06 16:05:32 1997 +0100 +++ b/src/HOL/RelPow.thy Thu Mar 06 16:06:08 1997 +0100 @@ -10,6 +10,9 @@ consts "^" :: "('a * 'a) set => nat => ('a * 'a) set" (infixr 100) -defs - rel_pow_def "R^n == nat_rec id (%m S. R O S) n" + +primrec "op ^" nat + "R^0 = id" + "R^(Suc n) = R O (R^n)" + end