# HG changeset patch
# User paulson
# Date 853498209 -3600
# Node ID 6ff9bd353121690e84ece8c28f858ebbe0492389
# Parent  ea8881e70f9c2153837fe7cd615e536469b179fa
Deleted the redundant theorem subset_empty_iff (subset_empty exists already)

diff -r ea8881e70f9c -r 6ff9bd353121 src/HOL/subset.ML
--- 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