# HG changeset patch
# User wenzelm
# Date 1709926109 -3600
# Node ID 7308e402451ff080e08763c29431a704ac34cb39
# Parent  11fa48986f37530cc2a3ddd40d40ee81844dfe08
more operations for Date and Time;

diff -r 11fa48986f37 -r 7308e402451f src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Fri Mar 08 20:03:21 2024 +0100
+++ b/src/Pure/General/date.scala	Fri Mar 08 20:28:29 2024 +0100
@@ -111,6 +111,10 @@
   def time: Time = Time.instant(instant)
   def timezone: ZoneId = rep.getZone
 
+  def + (t: Time): Date = Date(time + t, zone = timezone)
+  def - (t: Time): Date = Date(time - t, zone = timezone)
+  def - (d: Date): Time = time - d.time
+
   def format(fmt: Date.Format = Date.Format.default): String = fmt(this)
   override def toString: String = format()
 }