| changeset 12886 | 75ca1bf5ae12 |
| parent 12459 | 6978ab7cac64 |
| child 13462 | 56610e2ba220 |
--- a/src/HOL/Fun.ML Wed Feb 13 10:45:08 2002 +0100 +++ b/src/HOL/Fun.ML Wed Feb 13 10:48:29 2002 +0100 @@ -283,7 +283,7 @@ qed "inj_image_subset_iff"; Goal "inj f ==> (f`A = f`B) = (A = B)"; -by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1); +by (blast_tac (claset() addDs [injD]) 1); qed "inj_image_eq_iff"; Goal "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))";