| Thu, 09 Oct 2008 20:53:21 +0200 | wenzelm | moved future_scheduler flag to Concurrent/ROOT.ML; | changeset | files |
| Thu, 09 Oct 2008 20:53:20 +0200 | wenzelm | added invalidate_group; | changeset | files |
| Thu, 09 Oct 2008 20:53:17 +0200 | wenzelm | added fail-safe interrupt; | changeset | files |
| Thu, 09 Oct 2008 20:53:16 +0200 | wenzelm | subject to Multithreading.enabled; | changeset | files |
| Thu, 09 Oct 2008 20:53:15 +0200 | wenzelm | future result: Interrupt invalidates group, but pretends success otherwise; | changeset | files |
| Thu, 09 Oct 2008 20:53:14 +0200 | wenzelm | added future_scheduler flag (tmp!), from skip_proofs.ML; | changeset | files |
| Thu, 09 Oct 2008 20:53:13 +0200 | wenzelm | Dummy version of parallel list combinators -- plain sequential evaluation. | changeset | files |
| Thu, 09 Oct 2008 20:53:12 +0200 | wenzelm | added Concurrent/par_list_dummy.ML; | changeset | files |