# HG changeset patch
# User webertj
# Date 1140023409 -3600
# Node ID 6c0fca729f33ea8c3011f9636df6bdf761308fd7
# Parent  630b8dd0b31af958a27a1214eb340d5bfdd07f69
typo in a comment fixed

diff -r 630b8dd0b31a -r 6c0fca729f33 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Feb 15 17:09:45 2006 +0100
+++ b/src/HOL/arith_data.ML	Wed Feb 15 18:10:09 2006 +0100
@@ -461,7 +461,7 @@
    (l <= min m n + k) = (l <= m+k & l <= n+k)
 *)
 local
-(* a simpset for computations subject to optimazation !!! *)
+(* a simpset for computations subject to optimization !!! *)
 (*
 val binarith = map thm
   ["Pls_0_eq", "Min_1_eq",