equal
deleted
inserted
replaced
1 (* Title: Pure/Concurrent/par_list_dummy.ML |
1 (* Title: Pure/Concurrent/par_list_dummy.ML |
2 ID: $Id$ |
|
3 Author: Makarius |
2 Author: Makarius |
4 |
3 |
5 Dummy version of parallel list combinators -- plain sequential evaluation. |
4 Dummy version of parallel list combinators -- plain sequential evaluation. |
6 *) |
5 *) |
7 |
6 |
8 structure ParList: PAR_LIST = |
7 structure Par_List: PAR_LIST = |
9 struct |
8 struct |
10 |
9 |
11 val map = map; |
10 val map = map; |
12 val get_some = get_first; |
11 val get_some = get_first; |
13 val find_some = find_first; |
12 val find_some = find_first; |