src/HOL/Arith.ML
changeset 3396 aa74c71c3982
parent 3381 2bac33ec2b0d
child 3457 a8ab7c64817c
     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";