| changeset 13611 | 2edf034c902a |
| parent 13544 | 895994073bdf |
| child 13615 | 449a70d88b38 |
--- a/src/ZF/equalities.thy Mon Sep 30 16:44:00 2002 +0200 +++ b/src/ZF/equalities.thy Mon Sep 30 16:47:03 2002 +0200 @@ -491,7 +491,7 @@ apply (simp add: Inter_def) apply (subgoal_tac "ALL x:A. x~=0") prefer 2 apply blast -apply force +apply (tactic "first_best_tac (claset() addss' simpset()) 1") done lemma INT_UN_eq: "(ALL x:A. B(x) ~= 0)