# HG changeset patch
# User paulson
# Date 884255086 -3600
# Node ID 16f5efe9812da3175c67e875d0484a502323247b
# Parent  0218c486cf078c2721784ab544000a62bb2d9cb6
New rule: image_subset

diff -r 0218c486cf07 -r 16f5efe9812d src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Jan 08 11:23:18 1998 +0100
+++ b/src/HOL/Set.ML	Thu Jan 08 11:24:46 1998 +0100
@@ -612,6 +612,13 @@
 by (Blast_tac 1);
 qed "image_iff";
 
+(*This rewrite rule would confuse users if made default.*)
+goal thy "(f``A <= B) = (ALL x:A. f(x): B)";
+by (Blast_tac 1);
+qed "image_subset_iff";
+
+(*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
+  many existing proofs.*)
 val prems = goal thy "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
 by (blast_tac (claset() addIs prems) 1);
 qed "image_subsetI";