Ran expandshort and changed spelling of Grabczewski

--- 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 +

--- 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

--- 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.

--- 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
 *)

--- 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

--- 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

--- 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. 
 *)

--- 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.

--- 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".
 

--- 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
 *)