diff -r af954161e1cd -r 4bc306cb2832 src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Mon Dec 13 19:39:12 2021 +0100
+++ b/src/Pure/General/date.scala	Mon Dec 13 22:12:48 2021 +0100
@@ -13,6 +13,7 @@
 import java.time.temporal.TemporalAccessor
 
 import scala.annotation.tailrec
+import scala.math.Ordering
 
 
 object Date
@@ -74,6 +75,21 @@
   }
 
 
+  /* ordering */
+
+  object Ordering extends scala.math.Ordering[Date]
+  {
+    def compare(date1: Date, date2: Date): Int =
+      date1.instant.compareTo(date2.instant)
+  }
+
+  object Rev_Ordering extends scala.math.Ordering[Date]
+  {
+    def compare(date1: Date, date2: Date): Int =
+      date2.instant.compareTo(date1.instant)
+  }
+
+
   /* date operations */
 
   def timezone_utc: ZoneId = ZoneId.of("UTC")