--- 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);