# HG changeset patch
# User paulson
# Date 912005513 -3600
# Node ID e259383583186e918f0fd5be6d05caf017ef7ef6
# Parent  60f80b2a27771327f0ae13d424ccc2e9aa34e3a2
image_id in simpset

diff -r 60f80b2a2777 -r e25938358318 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Wed Nov 25 14:11:24 1998 +0100
+++ b/src/HOL/equalities.ML	Wed Nov 25 15:51:53 1998 +0100
@@ -108,6 +108,7 @@
 Goal "(%x. x) `` Y = Y";
 by (Blast_tac 1);
 qed "image_id";
+Addsimps [image_id];
 
 Goal "f``(g``A) = (%x. f (g x)) `` A";
 by (Blast_tac 1);