# HG changeset patch
# User wenzelm
# Date 1644404761 -3600
# Node ID fe81645c0b406638ff8c1158fbb2d252087e4fd5
# Parent  7cadf5a7ed5bc9165322e8df069739d571a9ec78
more operations;

diff -r 7cadf5a7ed5b -r fe81645c0b40 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Wed Feb 09 10:47:34 2022 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Wed Feb 09 12:06:01 2022 +0100
@@ -3334,8 +3334,15 @@
 
 newtype Time = Time Int
 
-instance Eq Time where Time ms1 == Time ms2 = ms1 == ms2
-instance Ord Time where compare (Time ms1) (Time ms2) = compare ms1 ms2
+instance Eq Time where Time a == Time b = a == b
+instance Ord Time where compare (Time a) (Time b) = compare a b
+instance Num Time where
+  fromInteger = Time . fromInteger
+  Time a + Time b = Time (a + b)
+  Time a - Time b = Time (a - b)
+  Time a * Time b = Time (a * b)
+  abs (Time a) = Time (abs a)
+  signum (Time a) = Time (signum a)
 
 seconds :: Double -> Time
 seconds s = Time (round (s * 1000.0))