src/ZF/UNITY/AllocBase.thy

--- a/src/ZF/UNITY/AllocBase.thy	Wed Jul 09 12:41:47 2003 +0200
+++ b/src/ZF/UNITY/AllocBase.thy	Thu Jul 10 17:14:41 2003 +0200
@@ -88,10 +88,7 @@
 
 lemma INT_Nclient_iff [iff]:
      "b\<in>Inter(RepFun(Nclients, B)) <-> (\<forall>x\<in>Nclients. b\<in>B(x))"
-apply (auto simp add: INT_iff)
-apply (rule_tac x = 0 in exI)
-apply (rule ltD, auto)
-done
+by (force simp add: INT_iff)
 
 lemma setsum_fun_mono [rule_format]:
      "n\<in>nat ==>