--- 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];
--- 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)";
--- 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...**)