src/HOL/Relation.ML
changeset 5998 b2ecd577b8a3
parent 5995 450cd1f0270b
child 6005 45186ec4d8b6
--- 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";