--- a/src/ZF/AC/AC15_WO6.thy Tue Sep 27 22:57:30 2022 +0100
+++ b/src/ZF/AC/AC15_WO6.thy Wed Sep 28 11:00:13 2022 +0200
@@ -16,7 +16,7 @@
So we don't have to prove all implications of both cases.
Moreover we don't need to prove AC13(1) \<Longrightarrow> AC1 and AC11 \<Longrightarrow> AC14 as
-Rubin \<and> Rubin do.
+Rubin & Rubin do.
*)
theory AC15_WO6
@@ -251,7 +251,7 @@
by (unfold AC13_def AC14_def AC15_def, fast)
(* ********************************************************************** *)
-(* The redundant proofs; however cited by Rubin \<and> Rubin *)
+(* The redundant proofs; however cited by Rubin & Rubin *)
(* ********************************************************************** *)
(* ********************************************************************** *)
--- a/src/ZF/AC/AC17_AC1.thy Tue Sep 27 22:57:30 2022 +0100
+++ b/src/ZF/AC/AC17_AC1.thy Wed Sep 28 11:00:13 2022 +0200
@@ -13,7 +13,7 @@
(** AC0 is equivalent to AC1.
- AC0 comes from Suppes, AC1 from Rubin \<and> Rubin **)
+ AC0 comes from Suppes, AC1 from Rubin & Rubin **)
lemma AC0_AC1_lemma: "\<lbrakk>f:(\<Prod>X \<in> A. X); D \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>g. g:(\<Prod>X \<in> D. X)"
by (fast intro!: lam_type apply_type)
@@ -262,7 +262,7 @@
(* ********************************************************************** *)
-(* AC5 \<Longrightarrow> AC4, Rubin \<and> Rubin, p. 11 *)
+(* AC5 \<Longrightarrow> AC4, Rubin & Rubin, p. 11 *)
(* ********************************************************************** *)
lemma AC5_AC4_aux1: "R \<subseteq> A*B \<Longrightarrow> (\<lambda>x \<in> R. fst(x)) \<in> R -> A"
--- a/src/ZF/AC/AC7_AC9.thy Tue Sep 27 22:57:30 2022 +0100
+++ b/src/ZF/AC/AC7_AC9.thy Wed Sep 28 11:00:13 2022 +0200
@@ -48,7 +48,7 @@
by (unfold AC6_def AC7_def, blast)
(* ********************************************************************** *)
-(* AC7 \<Longrightarrow> AC6, Rubin \<and> Rubin p. 12, Theorem 2.8 *)
+(* AC7 \<Longrightarrow> AC6, Rubin & Rubin p. 12, Theorem 2.8 *)
(* The case of the empty family of sets added in order to complete *)
(* the proof. *)
(* ********************************************************************** *)
@@ -104,7 +104,7 @@
(* ********************************************************************** *)
(* AC8 \<Longrightarrow> AC9 *)
-(* - this proof replaces the following two from Rubin \<and> Rubin: *)
+(* - this proof replaces the following two from Rubin & Rubin: *)
(* AC8 \<Longrightarrow> AC1 and AC1 \<Longrightarrow> AC9 *)
(* ********************************************************************** *)
@@ -124,7 +124,7 @@
(* ********************************************************************** *)
(* AC9 \<Longrightarrow> AC1 *)
(* The idea of this proof comes from "Equivalents of the Axiom of Choice" *)
-(* by Rubin \<and> Rubin. But (x * y) is not necessarily equipollent to *)
+(* by Rubin & Rubin. But (x * y) is not necessarily equipollent to *)
(* (x * y) \<union> {0} when y is a set of total functions acting from nat to *)
(* \<Union>(A) -- therefore we have used the set (y * nat) instead of y. *)
(* ********************************************************************** *)
--- a/src/ZF/AC/WO1_WO7.thy Tue Sep 27 22:57:30 2022 +0100
+++ b/src/ZF/AC/WO1_WO7.thy Wed Sep 28 11:00:13 2022 +0200
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, CU Computer Laboratory
Copyright 1998 University of Cambridge
-WO7 \<longleftrightarrow> LEMMA \<longleftrightarrow> WO1 (Rubin \<and> Rubin p. 5)
+WO7 \<longleftrightarrow> LEMMA \<longleftrightarrow> WO1 (Rubin & Rubin p. 5)
LEMMA is the sentence denoted by (**)
Also, WO1 \<longleftrightarrow> WO8
@@ -93,14 +93,14 @@
(* ********************************************************************** *)
-(* The proof of WO8 \<longleftrightarrow> WO1 (Rubin \<and> Rubin p. 6) *)
+(* The proof of WO8 \<longleftrightarrow> WO1 (Rubin & Rubin p. 6) *)
(* ********************************************************************** *)
lemma WO1_WO8: "WO1 \<Longrightarrow> WO8"
by (unfold WO1_def WO8_def, fast)
-(* The implication "WO8 \<Longrightarrow> WO1": a faithful image of Rubin \<and> Rubin's proof*)
+(* The implication "WO8 \<Longrightarrow> WO1": a faithful image of Rubin & Rubin's proof*)
lemma WO8_WO1: "WO8 \<Longrightarrow> WO1"
unfolding WO1_def WO8_def
apply (rule allI)
--- a/src/ZF/AC/WO2_AC16.thy Tue Sep 27 22:57:30 2022 +0100
+++ b/src/ZF/AC/WO2_AC16.thy Wed Sep 28 11:00:13 2022 +0200
@@ -9,7 +9,7 @@
The first instance is trivial, the third not difficult, but the second
is very complicated requiring many lemmas.
We also need to prove that at any stage gamma the set
-(s - \<Union>(...) - k_gamma) (Rubin \<and> Rubin page 15)
+(s - \<Union>(...) - k_gamma) (Rubin & Rubin page 15)
contains m distinct elements (in fact is equipollent to s)
*)
@@ -148,7 +148,7 @@
First quite complicated proof of the fact used in the recursive construction
of the family T_gamma (WO2 \<Longrightarrow> AC16(k #+ m, k)) - the fact that at any stage
gamma the set (s - \<Union>(...) - k_gamma) is equipollent to s
- (Rubin \<and> Rubin page 15).
+ (Rubin & Rubin page 15).
*)
(* ********************************************************************** *)
--- a/src/ZF/AC/WO6_WO1.thy Tue Sep 27 22:57:30 2022 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Wed Sep 28 11:00:13 2022 +0200
@@ -5,7 +5,7 @@
The only hard one is WO6 \<Longrightarrow> WO1.
Every proof (except WO6 \<Longrightarrow> WO1 and WO1 \<Longrightarrow> WO2) are described as "clear"
-by Rubin \<and> Rubin (page 2).
+by Rubin & Rubin (page 2).
They refer reader to a book by Gödel to see the proof WO1 \<Longrightarrow> WO2.
Fortunately order types made this proof also very easy.
*)
@@ -127,7 +127,7 @@
(* **********************************************************************
The proof of "WO6 \<Longrightarrow> WO1". Simplified by L C Paulson.
- From the book "Equivalents of the Axiom of Choice" by Rubin \<and> Rubin,
+ From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin,
pages 2-5
************************************************************************* *)
@@ -439,7 +439,7 @@
done
(* ********************************************************************** *)
-(* Rubin \<and> Rubin wrote, *)
+(* Rubin & Rubin wrote, *)
(* "It follows from (ii) and mathematical induction that if y*y \<subseteq> y then *)
(* y can be well-ordered" *)
--- a/src/ZF/Induct/PropLog.thy Tue Sep 27 22:57:30 2022 +0100
+++ b/src/ZF/Induct/PropLog.thy Wed Sep 28 11:00:13 2022 +0200
@@ -1,5 +1,5 @@
(* Title: ZF/Induct/PropLog.thy
- Author: Tobias Nipkow \<and> Lawrence C Paulson
+ Author: Tobias Nipkow & Lawrence C Paulson
Copyright 1993 University of Cambridge
*)
--- a/src/ZF/ex/Commutation.thy Tue Sep 27 22:57:30 2022 +0100
+++ b/src/ZF/ex/Commutation.thy Wed Sep 28 11:00:13 2022 +0200
@@ -1,5 +1,5 @@
(* Title: ZF/ex/Commutation.thy
- Author: Tobias Nipkow \<and> Sidi Ould Ehmety
+ Author: Tobias Nipkow & Sidi Ould Ehmety
Copyright 1995 TU Muenchen
Commutation theory for proving the Church Rosser theorem.
--- a/src/ZF/ex/NatSum.thy Tue Sep 27 22:57:30 2022 +0100
+++ b/src/ZF/ex/NatSum.thy Wed Sep 28 11:00:13 2022 +0200
@@ -1,5 +1,5 @@
(* Title: ZF/ex/NatSum.thy
- Author: Tobias Nipkow \<and> Lawrence C Paulson
+ Author: Tobias Nipkow & Lawrence C Paulson
A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.