improved comment;
authorwenzelm
Wed Dec 24 12:20:54 1997 +0100 (1997-12-24)
changeset 4479708d7c26db5b
parent 4478 9c5a0eef74ff
child 4480 d26e28c52788
improved comment;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Dec 24 10:42:27 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Dec 24 12:20:54 1997 +0100
     1.3 @@ -729,6 +729,7 @@
     1.4    | rev_order EQUAL = EQUAL
     1.5    | rev_order GREATER = LESS;
     1.6  
     1.7 +(*assume rel is a linear strict order*)
     1.8  fun make_ord rel (x, y) =
     1.9    if rel (x, y) then LESS
    1.10    else if rel (y, x) then GREATER