# HG changeset patch
# User ballarin
# Date 1051720421 -7200
# Node ID 2ae108fcd068165811c880b8528b2ceae2e752fe
# Parent  c6779865305629bc60d07d0013d4567eab121111
Unknown change.

diff -r c67798653056 -r 2ae108fcd068 src/Provers/linorder.ML
--- a/src/Provers/linorder.ML	Wed Apr 30 18:32:06 2003 +0200
+++ b/src/Provers/linorder.ML	Wed Apr 30 18:33:41 2003 +0200
@@ -40,7 +40,7 @@
 sig
   val less_reflE: thm  (* x < x ==> P *)
   val le_refl: thm  (* x <= x *)
-  val less_imp_le: thm (* x <= y ==> x < y *)
+  val less_imp_le: thm (* x < y ==> x <= y *)
   val not_lessI: thm (* y <= x  ==> ~(x < y) *)
   val not_leI: thm (* y < x  ==> ~(x <= y) *)
   val not_lessD: thm (* ~(x < y) ==> y <= x *)