diff timer.urs @ 0:37eefd0a2ed4
Import code from elsewhere
author |
Adam Chlipala <adam@chlipala.net> |
date |
Tue, 14 Dec 2010 10:55:22 -0500 |
parents |
|
children |
|
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/timer.urs Tue Dec 14 10:55:22 2010 -0500
@@ -0,0 +1,7 @@
+(** Cancelable delayed actions *)
+
+type t
+
+val create : {Milliseconds : int,
+ Action : transaction {}} -> transaction t
+val cancel : t -> transaction {}