# HG changeset patch
# User wenzelm
# Date 1664355613 -7200
# Node ID cf7db6353322cfc5e10d33c05bd21fc1fea69991
# Parent  728f38b016c05fb8f525467ce9d403b194aafaa6
recover informal "&" from 0c18df79b1c8;

diff -r 728f38b016c0 -r cf7db6353322 src/ZF/AC/AC15_WO6.thy
--- 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                   *)
 (* ********************************************************************** *)
 
 (* ********************************************************************** *)
diff -r 728f38b016c0 -r cf7db6353322 src/ZF/AC/AC17_AC1.thy
--- 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"
diff -r 728f38b016c0 -r cf7db6353322 src/ZF/AC/AC7_AC9.thy
--- 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.     *)
 (* ********************************************************************** *)
diff -r 728f38b016c0 -r cf7db6353322 src/ZF/AC/WO1_WO7.thy
--- 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)
diff -r 728f38b016c0 -r cf7db6353322 src/ZF/AC/WO2_AC16.thy
--- 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).
 *)
 
 (* ********************************************************************** *)
diff -r 728f38b016c0 -r cf7db6353322 src/ZF/AC/WO6_WO1.thy
--- 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"                                                 *)
 
diff -r 728f38b016c0 -r cf7db6353322 src/ZF/Induct/PropLog.thy
--- 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
 *)
 
diff -r 728f38b016c0 -r cf7db6353322 src/ZF/ex/Commutation.thy
--- 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.
diff -r 728f38b016c0 -r cf7db6353322 src/ZF/ex/NatSum.thy
--- 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.