| changeset 7499 | 23e090051cb8 |
| parent 6176 | 707b6f9859d2 |
| child 8127 | 68c6159440f1 |
--- a/src/ZF/Cardinal.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/Cardinal.ML Tue Sep 07 10:40:58 1999 +0200 @@ -650,7 +650,7 @@ qed "Diff_sing_eqpoll"; Goal "[| A lepoll 1; a:A |] ==> A = {a}"; -by (forward_tac [Diff_sing_lepoll] 1); +by (ftac Diff_sing_lepoll 1); by (assume_tac 1); by (dtac lepoll_0_is_0 1); by (blast_tac (claset() addEs [equalityE]) 1);