better version of Image_diag
authorpaulson
Tue Dec 01 10:39:02 1998 +0100 (1998-12-01)
changeset 5998b2ecd577b8a3
parent 5997 4d00bbd3d3ac
child 5999 84fe61a08c17
better version of Image_diag
src/HOL/Relation.ML
     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