src/Pure/Concurrent/par_list_dummy.ML
author wenzelm
Tue, 28 Jul 2009 14:54:53 +0200
changeset 32251 e586c82fdf69
parent 29368 503ce3f8f092
permissions -rw-r--r--
group status: Synchronized.var;
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;