src/Pure/Concurrent/par_list_dummy.ML
author haftmann
Wed, 11 Mar 2009 08:45:57 +0100
changeset 30432 aad3cd70e25a
parent 29368 503ce3f8f092
permissions -rw-r--r--
merged
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
    Author:     Makarius
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     3
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     4
Dummy version of parallel list combinators -- plain sequential evaluation.
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     5
*)
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     6
29368
503ce3f8f092 renamed structure ParList to Par_List;
wenzelm
parents: 28556
diff changeset
     7
structure Par_List: PAR_LIST =
28546
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     8
struct
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
     9
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    10
val map = map;
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    11
val get_some = get_first;
28556
85d2972fe9e6 fixed spelling;
wenzelm
parents: 28546
diff changeset
    12
val find_some = find_first;
28546
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    13
val exists = exists;
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    14
val forall = forall;
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    15
d57bfb44c9e5 Dummy version of parallel list combinators -- plain sequential evaluation.
wenzelm
parents:
diff changeset
    16
end;