equal
deleted
inserted
replaced
1 (* Title: Pure/Concurrent/future.ML |
1 (* Title: Pure/Concurrent/future.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Future values, see also |
4 Future values, see also |
5 http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf |
5 http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf |
|
6 http://www4.in.tum.de/~wenzelm/papers/parallel-ml.pdf |
6 |
7 |
7 Notes: |
8 Notes: |
8 |
9 |
9 * Futures are similar to delayed evaluation, i.e. delay/force is |
10 * Futures are similar to delayed evaluation, i.e. delay/force is |
10 generalized to fork/join (and variants). The idea is to model |
11 generalized to fork/join (and variants). The idea is to model |