# HG changeset patch
# User paulson
# Date 835108728 -7200
# Node ID b03dba9116d431d00181c29910b1fa21161c3d05
# Parent  cd3ffa5f1e311c4048d1a138836dd7377a4842d7
New rewrites for vacuous quantification

diff -r cd3ffa5f1e31 -r b03dba9116d4 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Jun 18 16:37:47 1996 +0200
+++ b/src/HOL/Set.ML	Tue Jun 18 16:38:48 1996 +0200
@@ -72,8 +72,9 @@
 (*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
 goal Set.thy "(! x:A. True) = True";
 by (REPEAT (ares_tac [TrueI,ballI,iffI] 1));
-qed "ball_rew";
-Addsimps [ball_rew];
+qed "ball_True";
+
+Addsimps [ball_True];
 
 (** Congruence rules **)
 
@@ -290,6 +291,15 @@
 qed_goal "empty_iff" Set.thy "(c : {}) = False"
  (fn _ => [ (fast_tac (!claset addSEs [emptyE]) 1) ]);
 
+goal Set.thy "Ball {} P = True";
+by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Ball_def, empty_def]) 1);
+qed "ball_empty";
+
+goal Set.thy "Bex {} P = False";
+by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Bex_def, empty_def]) 1);
+qed "bex_empty";
+Addsimps [ball_empty, bex_empty];
+
 
 section "Augmenting a set -- insert";