src/HOL/Set.ML

--- a/src/HOL/Set.ML	Wed Feb 12 15:43:50 1997 +0100
+++ b/src/HOL/Set.ML	Wed Feb 12 18:53:59 1997 +0100
@@ -341,6 +341,18 @@
 qed "bex_empty";
 Addsimps [ball_empty, bex_empty];
 
+goalw Set.thy [Ball_def] "(!x:A.False) = (A = {})";
+by(Fast_tac 1);
+qed "ball_False";
+Addsimps [ball_False];
+
+(* The dual is probably not helpful:
+goal Set.thy "(? x:A.True) = (A ~= {})";
+by(Fast_tac 1);
+qed "bex_True";
+Addsimps [bex_True];
+*)
+
 
 section "Augmenting a set -- insert";