author | wenzelm |
Wed, 31 Dec 2008 00:08:11 +0100 | |
changeset 29264 | 4ea3358fac3f |
parent 28556 | 85d2972fe9e6 |
child 29368 | 503ce3f8f092 |
permissions | -rw-r--r-- |
28546
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Concurrent/par_list_dummy.ML |
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
4 |
|
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
5 |
Dummy version of parallel list combinators -- plain sequential evaluation. |
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
6 |
*) |
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
7 |
|
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
8 |
structure ParList: PAR_LIST = |
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
9 |
struct |
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
10 |
|
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
11 |
val map = map; |
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
12 |
val get_some = get_first; |
28556 | 13 |
val find_some = find_first; |
28546
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
14 |
val exists = exists; |
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
15 |
val forall = forall; |
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
16 |
|
d57bfb44c9e5
Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff
changeset
|
17 |
end; |