src/HOL/Relation.ML
changeset 5998 b2ecd577b8a3
parent 5995 450cd1f0270b
child 6005 45186ec4d8b6
     1.1 --- a/src/HOL/Relation.ML	Mon Nov 30 10:45:39 1998 +0100
     1.2 +++ b/src/HOL/Relation.ML	Tue Dec 01 10:39:02 1998 +0100
     1.3 @@ -294,7 +294,7 @@
     1.4  by (Blast_tac 1);
     1.5  qed "Image_Id";
     1.6  
     1.7 -Goal "B<=A ==> diag A ^^ B = B";
     1.8 +Goal "diag A ^^ B = A Int B";
     1.9  by (Blast_tac 1);
    1.10  qed "Image_diag";
    1.11