changeset 4761 | 1681b32dd134 |
parent 4159 | 4aff9b7e5597 |
child 5144 | 7ac22e5a05d7 |
--- a/src/HOL/Set.thy Mon Mar 30 21:05:25 1998 +0200 +++ b/src/HOL/Set.thy Mon Mar 30 21:06:09 1998 +0200 @@ -18,7 +18,7 @@ set :: (term) term instance - set :: (term) {ord, minus, power} + set :: (term) {ord, minus, power} (* only ('a * 'a) set should be in power! *) syntax "op :" :: ['a, 'a set] => bool ("op :")