# 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 :")