# HG changeset patch # User oheimb # Date 891284769 -7200 # Node ID 1681b32dd13488177e73e7afd7db61f761981cc8 # Parent 9cdbd5a1d25aa71ccefc0d47daf61dd00dd6fb19 added caveat diff -r 9cdbd5a1d25a -r 1681b32dd134 src/HOL/Set.thy --- 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 :")