# HG changeset patch
# User paulson
# Date 828101798 -3600
# Node ID 26570790f089b7dc55f896f16e7baed8049109d2
# Parent  8c84606672fe922825e001be2025b3b932806279
new lemma for mutilated chess board

diff -r 8c84606672fe -r 26570790f089 src/HOL/subset.ML
--- 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