author | wenzelm |
Wed, 10 Dec 2008 22:05:58 +0100 | |
changeset 29055 | edaef19665e6 |
parent 28574 | e73db43298a6 |
child 29071 | 618216c658bb |
permissions | -rw-r--r-- |
(* Title: Pure/Concurrent/ROOT.ML ID: $Id$ Concurrency within the ML runtime. *) val future_scheduler = ref false; use "simple_thread.ML"; use "synchronized.ML"; use "mailbox.ML"; use "schedule.ML"; use "task_queue.ML"; use "future.ML"; use "par_list.ML"; if Multithreading.available then () else use "par_list_dummy.ML";