New theorem Image_id

--- a/src/HOL/Relation.ML	Thu Feb 05 10:47:29 1998 +0100
+++ b/src/HOL/Relation.ML	Thu Feb 05 10:48:43 1998 +0100
@@ -178,6 +178,12 @@
 
 Addsimps [Image_empty];
 
+goal thy "id ^^ A = A";
+by (Blast_tac 1);
+qed "Image_id";
+
+Addsimps [Image_id];
+
 qed_goal "Image_Int_subset" Relation.thy
     "R ^^ (A Int B) <= R ^^ A Int R ^^ B"
  (fn _ => [ Blast_tac 1 ]);