| changeset 2493 | bdeb5024353a |
| parent 2469 | b50b8c0eec01 |
| child 2496 | 40efb87985b5 |
--- a/src/ZF/Epsilon.ML Wed Jan 08 15:03:53 1997 +0100 +++ b/src/ZF/Epsilon.ML Wed Jan 08 15:04:27 1997 +0100 @@ -112,7 +112,7 @@ goalw Epsilon.thy [Transset_def] "!!i j. [| Transset(i); j:i |] ==> Memrel(i)-``{j} = j"; -by (fast_tac (eq_cs addSIs [MemrelI] addSEs [MemrelE]) 1); +by (fast_tac (!claset addSIs [MemrelI] addSEs [MemrelE]) 1); qed "under_Memrel"; (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)