# HG changeset patch
# User lcp
# Date 806922142 -7200
# Node ID a39bec9716845275b2ec37549d0f78a767d2c492
# Parent  968cd786a748328ecdc00accde496fb27ab41991
Ran expandshort and changed spelling of Grabczewski

diff -r 968cd786a748 -r a39bec971684 src/ZF/AC/AC16_WO4.thy
--- a/src/ZF/AC/AC16_WO4.thy	Thu Jul 27 18:28:14 1995 +0200
+++ b/src/ZF/AC/AC16_WO4.thy	Fri Jul 28 11:02:22 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/AC16_WO4.thy
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 *)
 
 AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux +
diff -r 968cd786a748 -r a39bec971684 src/ZF/AC/AC18_AC19.thy
--- a/src/ZF/AC/AC18_AC19.thy	Thu Jul 27 18:28:14 1995 +0200
+++ b/src/ZF/AC/AC18_AC19.thy	Fri Jul 28 11:02:22 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/AC18_AC19.thy
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 Additional definition used in the proof AC19 ==> AC1 which is a part
 of the chain AC1 ==> AC18 ==> AC19 ==> AC1
@@ -15,4 +15,4 @@
 
   u_def "u_(a) == {c Un {0}. c:a}"
 
-end
\ No newline at end of file
+end
diff -r 968cd786a748 -r a39bec971684 src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Thu Jul 27 18:28:14 1995 +0200
+++ b/src/ZF/AC/AC_Equiv.thy	Fri Jul 28 11:02:22 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/AC_Equiv.thy
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 Axioms AC1 -- AC19 come from "Equivalents of the Axiom of Choice, II"
 by H. Rubin and J.E. Rubin, 1985.
diff -r 968cd786a748 -r a39bec971684 src/ZF/AC/DC.thy
--- a/src/ZF/AC/DC.thy	Thu Jul 27 18:28:14 1995 +0200
+++ b/src/ZF/AC/DC.thy	Fri Jul 28 11:02:22 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/DC.thy
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 Theory file for the proofs concernind the Axiom of Dependent Choice
 *)
diff -r 968cd786a748 -r a39bec971684 src/ZF/AC/HH.thy
--- a/src/ZF/AC/HH.thy	Thu Jul 27 18:28:14 1995 +0200
+++ b/src/ZF/AC/HH.thy	Fri Jul 28 11:02:22 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/HH.thy
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 The theory file for the proofs of
   AC17 ==> AC1
diff -r 968cd786a748 -r a39bec971684 src/ZF/AC/Hartog.thy
--- a/src/ZF/AC/Hartog.thy	Thu Jul 27 18:28:14 1995 +0200
+++ b/src/ZF/AC/Hartog.thy	Fri Jul 28 11:02:22 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/Hartog.thy
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 Hartog's function.
 *)
@@ -15,4 +15,4 @@
 
   Hartog_def "Hartog(X) == LEAST i. ~i lepoll X"
 
-end
\ No newline at end of file
+end
diff -r 968cd786a748 -r a39bec971684 src/ZF/AC/OrdQuant.thy
--- a/src/ZF/AC/OrdQuant.thy	Thu Jul 27 18:28:14 1995 +0200
+++ b/src/ZF/AC/OrdQuant.thy	Fri Jul 28 11:02:22 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/OrdQuant.thy
     ID:         $Id$
-    Authors: 	Krzysztof Gr`abczewski and L C Paulson
+    Authors: 	Krzysztof Grabczewski and L C Paulson
 
 Quantifiers and union operator for ordinals. 
 *)
diff -r 968cd786a748 -r a39bec971684 src/ZF/AC/Transrec2.thy
--- a/src/ZF/AC/Transrec2.thy	Thu Jul 27 18:28:14 1995 +0200
+++ b/src/ZF/AC/Transrec2.thy	Fri Jul 28 11:02:22 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/Transrec2.thy
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 Transfinite recursion introduced to handle definitions based on the three
 cases of ordinals.
diff -r 968cd786a748 -r a39bec971684 src/ZF/AC/WO6_WO1.thy
--- a/src/ZF/AC/WO6_WO1.thy	Thu Jul 27 18:28:14 1995 +0200
+++ b/src/ZF/AC/WO6_WO1.thy	Fri Jul 28 11:02:22 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/WO6_WO1.thy
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 The proof of "WO6 ==> WO1".
 
diff -r 968cd786a748 -r a39bec971684 src/ZF/AC/first.thy
--- a/src/ZF/AC/first.thy	Thu Jul 27 18:28:14 1995 +0200
+++ b/src/ZF/AC/first.thy	Fri Jul 28 11:02:22 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/first.thy
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
 Theory helpful in proofs using first element of a well ordered set
 *)