| changeset 9316 | e58778cc4d22 |
| parent 9190 | b86ff604729f |
| child 10186 | 499637e8f2c6 |
| 9315:f793f05024f6 | 9316:e58778cc4d22 |
|---|---|
79 choplev 0; |
79 choplev 0; |
80 by (best_tac (claset() addSEs [equalityCE]) 1); |
80 by (best_tac (claset() addSEs [equalityCE]) 1); |
81 qed ""; |
81 qed ""; |
82 |
82 |
83 |
83 |
84 (*** The Schroder-Berstein Theorem ***) |
84 (*** The Schroeder-Berstein Theorem ***) |
85 |
85 |
86 Goal "[| -(f``X) = g``(-X); f(a)=g(b); a:X |] ==> b:X"; |
86 Goal "[| -(f``X) = g``(-X); f(a)=g(b); a:X |] ==> b:X"; |
87 by (Blast_tac 1); |
87 by (Blast_tac 1); |
88 qed "disj_lemma"; |
88 qed "disj_lemma"; |
89 |
89 |