# HG changeset patch
# User paulson
# Date 865585238 -7200
# Node ID 02dc9c5b035fc6976194dc6021ed9c73fa4cc07e
# Parent  9092b79d86d50f4b4d408d00071772997f408df6
New miniscoping rules ball_triv and bex_triv

diff -r 9092b79d86d5 -r 02dc9c5b035f src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Jun 06 10:19:53 1997 +0200
+++ b/src/HOL/Set.ML	Fri Jun 06 10:20:38 1997 +0200
@@ -80,17 +80,17 @@
 AddIs  [bexI];
 AddSEs [bexE];
 
-(*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
-goalw Set.thy [Ball_def] "(! x:A. True) = True";
-by (Simp_tac 1);
-qed "ball_True";
+(*Trival rewrite rule*)
+goal Set.thy "(! x:A.P) = ((? x. x:A) --> P)";
+by (simp_tac (!simpset addsimps [Ball_def]) 1);
+qed "ball_triv";
 
 (*Dual form for existentials*)
-goalw Set.thy [Bex_def] "(? x:A. False) = False";
-by (Simp_tac 1);
-qed "bex_False";
+goal Set.thy "(? x:A.P) = ((? x. x:A) & P)";
+by (simp_tac (!simpset addsimps [Bex_def]) 1);
+qed "bex_triv";
 
-Addsimps [ball_True, bex_False];
+Addsimps [ball_triv, bex_triv];
 
 (** Congruence rules **)
 
@@ -234,18 +234,6 @@
 qed "bex_empty";
 Addsimps [ball_empty, bex_empty];
 
-goalw Set.thy [Ball_def] "(!x:A.False) = (A = {})";
-by(Blast_tac 1);
-qed "ball_False";
-Addsimps [ball_False];
-
-(* The dual is probably not helpful:
-goal Set.thy "(? x:A.True) = (A ~= {})";
-by(Blast_tac 1);
-qed "bex_True";
-Addsimps [bex_True];
-*)
-
 
 section "The Powerset operator -- Pow";