src/HOL/ex/set.ML
changeset 9316 e58778cc4d22
parent 9190 b86ff604729f
child 10186 499637e8f2c6
--- 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);