new lemma for mutilated chess board

--- a/src/HOL/subset.ML	Fri Mar 29 11:38:47 1996 +0100
+++ b/src/HOL/subset.ML	Fri Mar 29 13:16:38 1996 +0100
@@ -16,6 +16,9 @@
 by (fast_tac set_cs 1);
 qed "subset_insert";
 
+qed_goal "subset_empty_iff" Set.thy "(A<={}) = (A={})"
+ (fn _=> [ (fast_tac (set_cs addIs [equalityI]) 1) ]);
+
 (*** Big Union -- least upper bound of a set  ***)
 
 val prems = goal Set.thy