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