--- a/src/HOL/Arith.ML Wed Jun 04 12:26:42 1997 +0200
+++ b/src/HOL/Arith.ML Wed Jun 04 16:03:54 1997 +0200
@@ -366,7 +366,7 @@
by (ALLGOALS Asm_simp_tac);
qed "diff_diff_left";
-(*This and the next few suggested by Florian Kammüller*)
+(*This and the next few suggested by Florian Kammueller*)
goal Arith.thy "!!i::nat. i-j-k = i-k-j";
by (simp_tac (!simpset addsimps [diff_diff_left, add_commute]) 1);
qed "diff_commute";
--- a/src/HOL/Power.ML Wed Jun 04 12:26:42 1997 +0200
+++ b/src/HOL/Power.ML Wed Jun 04 16:03:54 1997 +0200
@@ -48,7 +48,7 @@
qed_spec_mp "power_less_dvd";
-(*** Binomial Coefficients, following Andy Gordon and Florian Kammüller ***)
+(*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
goal thy "(n choose 0) = 1";
by (exhaust_tac "n" 1);