eliminated non-ASCII;
authorwenzelm
Wed Jun 04 16:03:54 1997 +0200 (1997-06-04)
changeset 3396aa74c71c3982
parent 3395 d8700b008944
child 3397 3e2b8d0de2a0
eliminated non-ASCII;
src/HOL/Arith.ML
src/HOL/Power.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Jun 04 12:26:42 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Wed Jun 04 16:03:54 1997 +0200
     1.3 @@ -366,7 +366,7 @@
     1.4  by (ALLGOALS Asm_simp_tac);
     1.5  qed "diff_diff_left";
     1.6  
     1.7 -(*This and the next few suggested by Florian Kammüller*)
     1.8 +(*This and the next few suggested by Florian Kammueller*)
     1.9  goal Arith.thy "!!i::nat. i-j-k = i-k-j";
    1.10  by (simp_tac (!simpset addsimps [diff_diff_left, add_commute]) 1);
    1.11  qed "diff_commute";
     2.1 --- a/src/HOL/Power.ML	Wed Jun 04 12:26:42 1997 +0200
     2.2 +++ b/src/HOL/Power.ML	Wed Jun 04 16:03:54 1997 +0200
     2.3 @@ -48,7 +48,7 @@
     2.4  qed_spec_mp "power_less_dvd";
     2.5  
     2.6  
     2.7 -(*** Binomial Coefficients, following Andy Gordon and Florian Kammüller ***)
     2.8 +(*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
     2.9  
    2.10  goal thy "(n choose 0) = 1";
    2.11  by (exhaust_tac "n" 1);