changeset 5281 | f4d16517b360 |
parent 5278 | a903b66822e2 |
child 5316 | 7a8975451a89 |
--- a/src/HOL/equalities.ML Thu Aug 06 18:21:14 1998 +0200 +++ b/src/HOL/equalities.ML Sat Aug 08 14:00:56 1998 +0200 @@ -123,6 +123,11 @@ qed "image_is_empty"; AddIffs [image_is_empty]; +Goal "f `` {x. P x} = {f x | x. P x}"; +by(Blast_tac 1); +qed "image_Collect"; +Addsimps [image_Collect]; + Goalw [image_def] "(%x. if P x then f x else g x) `` S \ \ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";