author | paulson |
Mon, 18 Oct 1999 15:16:10 +0200 | |
changeset 7876 | 1b3b683c092e |
parent 7875 | 1baf422ec16a |
child 7877 | e5e019d60f71 |
src/HOL/Fun.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Fun.ML Sat Oct 16 18:56:09 1999 +0200 +++ b/src/HOL/Fun.ML Mon Oct 18 15:16:10 1999 +0200 @@ -253,6 +253,10 @@ qed "vimage_id"; Addsimps [vimage_ident, vimage_id]; +Goal "f -`` (f `` A) = {y. EX x:A. f x = f y}"; +by (blast_tac (claset() addIs [sym]) 1); +qed "vimage_image_eq"; + Goal "f``(A Int B) <= f``A Int f``B"; by (Blast_tac 1); qed "image_Int_subset";