# HG changeset patch
# User paulson
# Date 886672123 -3600
# Node ID 87fc0d44b83735c7a9f33e30d2dfa5358df29462
# Parent  e3e7e901ce6c34220658098c3af1b1f69be5acc1
New theorem Image_id

diff -r e3e7e901ce6c -r 87fc0d44b837 src/HOL/Relation.ML
--- 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 ]);