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];