--- 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) = {}";