# HG changeset patch
# User wenzelm
# Date 1451227963 -3600
# Node ID 2a9bed6cd6e5a78c39cfc190860bd03f5d7359e1
# Parent  c51ce9ed0b1c23eccda5f2cb6751eaf83ba245c6
tuned;

diff -r c51ce9ed0b1c -r 2a9bed6cd6e5 src/HOL/ex/Set_Theory.thy
--- a/src/HOL/ex/Set_Theory.thy	Sat Dec 26 19:37:06 2015 +0100
+++ b/src/HOL/ex/Set_Theory.thy	Sun Dec 27 15:52:43 2015 +0100
@@ -74,18 +74,18 @@
   by best
 
 
-subsection \<open>The Schröder-Berstein Theorem\<close>
+subsection \<open>The Schröder-Bernstein Theorem\<close>
 
-lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
+lemma disj_lemma: "- (f ` X) = g' ` (-X) \<Longrightarrow> f a = g' b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
   by blast
 
 lemma surj_if_then_else:
-  "-(f ` X) = g ` (-X) \<Longrightarrow> surj (\<lambda>z. if z \<in> X then f z else g z)"
+  "-(f ` X) = g' ` (-X) \<Longrightarrow> surj (\<lambda>z. if z \<in> X then f z else g' z)"
   by (simp add: surj_def) blast
 
 lemma bij_if_then_else:
-  "inj_on f X \<Longrightarrow> inj_on g (-X) \<Longrightarrow> -(f ` X) = g ` (-X) \<Longrightarrow>
-    h = (\<lambda>z. if z \<in> X then f z else g z) \<Longrightarrow> inj h \<and> surj h"
+  "inj_on f X \<Longrightarrow> inj_on g' (-X) \<Longrightarrow> -(f ` X) = g' ` (-X) \<Longrightarrow>
+    h = (\<lambda>z. if z \<in> X then f z else g' z) \<Longrightarrow> inj h \<and> surj h"
   apply (unfold inj_on_def)
   apply (simp add: surj_if_then_else)
   apply (blast dest: disj_lemma sym)