diff -r 7b84677315ed -r 450cd1f0270b src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Sun Nov 29 13:21:38 1998 +0100
+++ b/src/HOL/Relation.ML	Mon Nov 30 10:43:35 1998 +0100
@@ -54,7 +54,7 @@
 
 Goal "diag(A) <= A Times A";
 by (Blast_tac 1);
-qed "diag_subset_Sigma";
+qed "diag_subset_Times";
 
 
 
@@ -161,6 +161,11 @@
 qed "converse_Id";
 Addsimps [converse_Id];
 
+Goal "(diag A) ^-1 = diag A";
+by (Blast_tac 1);
+qed "converse_diag";
+Addsimps [converse_diag];
+
 (** Domain **)
 
 Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";
@@ -226,6 +231,11 @@
 qed "Range_Id";
 Addsimps [Range_Id];
 
+Goal "Range (diag A) = A";
+by Auto_tac;
+qed "Range_diag";
+Addsimps [Range_diag];
+
 Goal "Range(A Un B) = Range(A) Un Range(B)";
 by (Blast_tac 1);
 qed "Range_Un_eq";
@@ -284,7 +294,11 @@
 by (Blast_tac 1);
 qed "Image_Id";
 
-Addsimps [Image_Id];
+Goal "B<=A ==> diag A ^^ B = B";
+by (Blast_tac 1);
+qed "Image_diag";
+
+Addsimps [Image_Id, Image_diag];
 
 qed_goal "Image_Int_subset" thy
     "R ^^ (A Int B) <= R ^^ A Int R ^^ B"