DESCRIPTION manual: comment that we prefer to use < and <=

HOL-Theorem-Prover · May 11, 2023 · 81d4db3 · 81d4db3
1 parent 5a061b9
commit 81d4db3
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Manual/Description/theories.stex b/Manual/Description/theories.stex
@@ -1640,6 +1640,8 @@ A full set of comparison operators is defined in terms of \verb+<+.
 \end{alltt}
 \end{hol}
 
+Note that in all of \HOL{}'s standard numeric theories, it is usual practice to avoid uses of the ``greater-than'' constants and to express everything with either \holtxt{$<$} or \holtxt{$\le$}.
+
 \paragraph{Division and modulus}
 
 A constant specification is used to introduce division ({\small\verb+DIV+}, infix) and