# HG changeset patch
# User wenzelm
# Date 879171912 -3600
# Node ID 7f7bf0bd0f6345e1b240ff01c35ac7e124466e0c
# Parent  1c2553be18218f2bd43df79ebe7267699c9c3bf7
ASCII-fied;

diff -r 1c2553be1821 -r 7f7bf0bd0f63 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Mon Nov 10 15:06:58 1997 +0100
+++ b/src/HOL/Integ/Bin.ML	Mon Nov 10 15:25:12 1997 +0100
@@ -193,7 +193,7 @@
           norm_Bcons_Bcons];
 
 
-(** Simplification rules for comparison of binary numbers (Norbert Völker) **) 
+(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) 
 
 Addsimps [zadd_assoc];
 
diff -r 1c2553be1821 -r 7f7bf0bd0f63 src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Mon Nov 10 15:06:58 1997 +0100
+++ b/src/HOL/Integ/Equiv.ML	Mon Nov 10 15:25:12 1997 +0100
@@ -241,7 +241,7 @@
 qed "congruent2_commuteI";
 
 
-(*** Cardinality results suggested by Florian Kammüller ***)
+(*** Cardinality results suggested by Florian Kammueller ***)
 
 (*Recall that  equiv A r  implies  r <= A Times A   (equiv_type) *)
 goal thy "!!A. [| finite A; r <= A Times A |] ==> finite (A/r)";
diff -r 1c2553be1821 -r 7f7bf0bd0f63 src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Mon Nov 10 15:06:58 1997 +0100
+++ b/src/HOL/Integ/Integ.ML	Mon Nov 10 15:25:12 1997 +0100
@@ -757,7 +757,7 @@
 qed "zadd_zle_self";
 
 
-(**** Comparisons: lemmas and proofs by Norbert Völker ****)
+(**** Comparisons: lemmas and proofs by Norbert Voelker ****)
 
 (** One auxiliary theorem...**)