# HG changeset patch
# User wenzelm
# Date 963522832 -7200
# Node ID e58778cc4d22ccd7cc84c4276c81a19e1d3b3231
# Parent  f793f05024f6f2718ba2a259e8a0b7a315ab5e09
fixed comment;

diff -r f793f05024f6 -r e58778cc4d22 src/HOL/ex/set.ML
--- 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);