# 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);