# HG changeset patch
# User wenzelm
# Date 865433034 -7200
# Node ID aa74c71c39823afd6e6b6ec1712256dd3eef6ef9
# Parent  d8700b00894413a1849a4cff11e5cfd976737cc4
eliminated non-ASCII;

diff -r d8700b008944 -r aa74c71c3982 src/HOL/Arith.ML
--- 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";
diff -r d8700b008944 -r aa74c71c3982 src/HOL/Power.ML
--- 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);