src/HOL/subset.ML
changeset 2515 6ff9bd353121
parent 1761 29e08d527ba1
child 2893 2ee005e46d6d
--- 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