| changeset 7536 | 5c094aec523d |
| parent 7514 | 3235863a069a |
| child 7876 | 1b3b683c092e |
--- a/src/HOL/Fun.ML Fri Sep 10 17:28:51 1999 +0200 +++ b/src/HOL/Fun.ML Fri Sep 10 18:37:04 1999 +0200 @@ -67,6 +67,10 @@ by (Blast_tac 1); qed "image_compose"; +Goal "f``g``A = (UN x:A. {f (g x)})"; +by (Blast_tac 1); +qed "image_image_eq_UN"; + Goalw [o_def] "UNION A (g o f) = UNION (f``A) g"; by (Blast_tac 1); qed "UN_o";