From 81d4db31b01094f3d3dee3083d17be9d9707a209 Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Thu, 11 May 2023 11:17:11 +1000
Subject: [PATCH] DESCRIPTION manual: comment that we prefer to use < and <=

---
 Manual/Description/theories.stex | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Manual/Description/theories.stex b/Manual/Description/theories.stex
index 7e57b129d2..80b19292c0 100644
--- 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