# HG changeset patch
# User paulson
# Date 912505142 -3600
# Node ID b2ecd577b8a35de69555ba968106ce12056dff13
# Parent  4d00bbd3d3acd2f9372d45e94ff750e3fbb1234e
better version of Image_diag

diff -r 4d00bbd3d3ac -r b2ecd577b8a3 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Mon Nov 30 10:45:39 1998 +0100
+++ b/src/HOL/Relation.ML	Tue Dec 01 10:39:02 1998 +0100
@@ -294,7 +294,7 @@
 by (Blast_tac 1);
 qed "Image_Id";
 
-Goal "B<=A ==> diag A ^^ B = B";
+Goal "diag A ^^ B = A Int B";
 by (Blast_tac 1);
 qed "Image_diag";