| changeset 6301 | 08245f5a436d |
| parent 6290 | 31483ca40e91 |
| child 6829 | 50459a995aa3 |
--- a/src/HOL/Fun.ML Wed Mar 03 11:12:29 1999 +0100 +++ b/src/HOL/Fun.ML Wed Mar 03 11:15:18 1999 +0100 @@ -213,6 +213,14 @@ by Auto_tac; qed "inv_image_comp"; +Goal "inj f ==> (f a : f``A) = (a : A)"; +by (blast_tac (claset() addDs [injD]) 1); +qed "inj_image_mem_iff"; + +Goal "inj f ==> (f``A = f``B) = (A = B)"; +by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1); +qed "inj_image_eq_iff"; + val set_cs = claset() delrules [equalityI];