# HG changeset patch
# User paulson
# Date 879259556 -3600
# Node ID 5a2cd204f8b4fd94b752c44047faccb01bf8b703
# Parent  2b9fc1f0888687cf88a75de46e8d2292ed74d6c9
Rationalized the theorem if_image_distrib.
Added parens to not_empty.

diff -r 2b9fc1f08886 -r 5a2cd204f8b4 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue Nov 11 12:30:51 1997 +0100
+++ b/src/HOL/equalities.ML	Tue Nov 11 15:45:56 1997 +0100
@@ -111,7 +111,7 @@
 
 goalw thy [image_def]
 "(%x. if P x then f x else g x) `` S                    \
-\ = (f `` ({x. x:S & P x})) Un (g `` ({x. x:S & ~(P x)}))";
+\ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";
 by (split_tac [expand_if] 1);
 by (Blast_tac 1);
 qed "if_image_distrib";
@@ -369,7 +369,7 @@
 
 (*Basic identities*)
 
-val not_empty = prove_goal Set.thy "A ~= {} = (? x. x:A)" (K [Blast_tac 1]);
+val not_empty = prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]);
 (*Addsimps[not_empty];*)
 
 goal thy "(UN x:{}. B x) = {}";