--- a/src/HOL/ex/set.thy Fri Dec 03 20:26:57 2010 +0100
+++ b/src/HOL/ex/set.thy Fri Dec 03 20:38:58 2010 +0100
@@ -4,7 +4,7 @@
Copyright 1991 University of Cambridge
*)
-header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
+header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
theory set imports Main begin
@@ -73,7 +73,7 @@
by best
-subsection {* The Schröder-Berstein Theorem *}
+subsection {* The Schröder-Berstein Theorem *}
lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
by blast