# HG changeset patch
# User lcp
# Date 783623472 -3600
# Node ID 41b59e4c78c491a21e17a3903fb2c86de47a0e33
# Parent  023cef66815801485dfb3236636a53189913e3e1
ZF/domrange/image_subset: tidied

diff -r 023cef668158 -r 41b59e4c78c4 src/ZF/domrange.ML
--- a/src/ZF/domrange.ML	Mon Oct 31 18:09:32 1994 +0100
+++ b/src/ZF/domrange.ML	Mon Oct 31 18:11:12 1994 +0100
@@ -147,9 +147,7 @@
 
 val image_subset = prove_goal ZF.thy
     "!!A B r. r <= A*B ==> r``C <= B"
- (fn _ =>
-  [ (rtac subsetI 1),
-    (REPEAT (eresolve_tac [asm_rl, imageE, subsetD RS SigmaD2] 1)) ]);
+ (fn _ => [ (fast_tac (pair_cs addSEs [imageE]) 1) ]);
 
 
 (*** Inverse image of a set under a function/relation ***)