changeset 29564 | f8b933a62151 |
parent 28154 | 3c3663e24ba7 |
child 32736 | f126e68d003d |
29563:4773c5c994dc | 29564:f8b933a62151 |
---|---|
1 (* Title: Pure/ML-Systems/thread_dummy.ML |
1 (* Title: Pure/ML-Systems/thread_dummy.ML |
2 ID: $Id$ |
|
3 Author: Makarius |
2 Author: Makarius |
4 |
3 |
5 Default (mostly dummy) implementation of thread structures |
4 Default (mostly dummy) implementation of thread structures |
6 (cf. polyml/basis/Thread.sml). |
5 (cf. polyml/basis/Thread.sml). |
7 *) |
6 *) |