src/HOL/UNITY/UNITY.ML

 
 From Misra, "A Logic for Concurrent Programming", 1994
 *)
 
 set proof_timing;
+
+(*Perhaps equalities.ML shouldn't add this in the first place!*)
+Delsimps [image_Collect];
 
 
 (*** General lemmas ***)
 
 Goal "UNIV Times UNIV = UNIV";