Deleted the redundant theorem subset_empty_iff (subset_empty exists already)

--- a/src/HOL/subset.ML	Fri Jan 17 11:13:18 1997 +0100
+++ b/src/HOL/subset.ML	Fri Jan 17 11:50:09 1997 +0100
@@ -16,9 +16,6 @@
 by (Fast_tac 1);
 qed "subset_insert";
 
-qed_goal "subset_empty_iff" Set.thy "(A<={}) = (A={})"
- (fn _=> [ (Fast_tac 1) ]);
-
 (*** Big Union -- least upper bound of a set  ***)
 
 val prems = goal Set.thy