src/Pure/Concurrent/par_list_dummy.ML
author wenzelm
Thu, 09 Oct 2008 20:53:13 +0200
changeset 28546 d57bfb44c9e5
child 28556 85d2972fe9e6
permissions -rw-r--r--
Dummy version of parallel list combinators -- plain sequential evaluation.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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;
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    13
val fins_some = find_first;
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;