--- a/src/HOL/ex/set.ML Thu Jul 13 23:13:10 2000 +0200
+++ b/src/HOL/ex/set.ML Thu Jul 13 23:13:52 2000 +0200
@@ -81,7 +81,7 @@
qed "";
-(*** The Schroder-Berstein Theorem ***)
+(*** The Schroeder-Berstein Theorem ***)
Goal "[| -(f``X) = g``(-X); f(a)=g(b); a:X |] ==> b:X";
by (Blast_tac 1);