| changeset 5305 | 513925de8962 |
| parent 5266 | 1d11c7e4b999 |
| child 5316 | 7a8975451a89 |
--- a/src/HOL/Set.ML Wed Aug 12 16:21:18 1998 +0200 +++ b/src/HOL/Set.ML Wed Aug 12 16:23:25 1998 +0200 @@ -606,10 +606,6 @@ AddIs [image_eqI]; AddSEs [imageE]; -Goalw [o_def] "(f o g)``r = f``(g``r)"; -by (Blast_tac 1); -qed "image_compose"; - Goal "f``(A Un B) = f``A Un f``B"; by (Blast_tac 1); qed "image_Un";