src/HOL/UNITY/Alloc.ML
changeset 8948 b797cfa3548d
parent 8930 cb419b8498e5
child 8985 13ad7ce031bb
--- a/src/HOL/UNITY/Alloc.ML	Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/Alloc.ML	Wed May 24 18:40:01 2000 +0200
@@ -6,6 +6,9 @@
 Specification of Chandy and Charpentier's Allocator
 *)
 
+(*Perhaps equalities.ML shouldn't add this in the first place!*)
+Delsimps [image_Collect];
+
 AddIs [impOfSubs subset_preserves_o];
 Addsimps [funPair_o_distrib];
 Addsimps [Always_INT_distrib];