| changeset 15131 | c69542757a4d |
| parent 15112 | 6f0772a94299 |
| child 15140 | 322485b816ac |
--- a/src/HOL/Relation_Power.thy Mon Aug 16 14:21:54 2004 +0200 +++ b/src/HOL/Relation_Power.thy Mon Aug 16 14:22:27 2004 +0200 @@ -12,7 +12,9 @@ Examples: range(f^n) = A and Range(R^n) = B need constraints. *) -theory Relation_Power = Nat: +theory Relation_Power +import Nat +begin instance set :: (type) power .. (* only ('a * 'a) set should be in power! *)