--- a/src/Pure/Concurrent/mailbox.ML Thu Sep 04 21:02:42 2008 +0200
+++ b/src/Pure/Concurrent/mailbox.ML Thu Sep 04 21:12:06 2008 +0200
@@ -1,5 +1,6 @@
(* Title: Pure/Concurrent/mailbox.ML
ID: $Id$
+ Author: Makarius
Concurrent message exchange via mailbox -- with unbounded queueing.
*)
--- a/src/Pure/Concurrent/schedule.ML Thu Sep 04 21:02:42 2008 +0200
+++ b/src/Pure/Concurrent/schedule.ML Thu Sep 04 21:12:06 2008 +0200
@@ -1,5 +1,6 @@
(* Title: Pure/Concurrent/schedule.ML
ID: $Id$
+ Author: Makarius
Scheduling -- multiple threads working on a queue of tasks.
*)