src/HOL/Relation.ML
changeset 5998 b2ecd577b8a3
parent 5995 450cd1f0270b
child 6005 45186ec4d8b6
equal deleted inserted replaced
5997:4d00bbd3d3ac 5998:b2ecd577b8a3
   292 
   292 
   293 Goal "Id ^^ A = A";
   293 Goal "Id ^^ A = A";
   294 by (Blast_tac 1);
   294 by (Blast_tac 1);
   295 qed "Image_Id";
   295 qed "Image_Id";
   296 
   296 
   297 Goal "B<=A ==> diag A ^^ B = B";
   297 Goal "diag A ^^ B = A Int B";
   298 by (Blast_tac 1);
   298 by (Blast_tac 1);
   299 qed "Image_diag";
   299 qed "Image_diag";
   300 
   300 
   301 Addsimps [Image_Id, Image_diag];
   301 Addsimps [Image_Id, Image_diag];
   302 
   302