--- 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";