diff -r 58bd51302b21 -r fcf7f29a3447 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Jul 14 14:51:02 2000 +0200
+++ b/src/HOL/Set.ML	Fri Jul 14 16:27:37 2000 +0200
@@ -204,6 +204,8 @@
 by (rtac subset_refl 1);
 qed "equalityD2";
 
+(*Be careful when adding this to the claset as subset_empty is in the simpset:
+  A={} goes to {}<=A and A<={} and then back to A={} !*)
 val prems = Goal
     "[| A = B;  [| A<=B; B<=(A::'a set) |] ==> P |]  ==>  P";
 by (resolve_tac prems 1);