src/Pure/Concurrent/par_list_sequential.ML
author wenzelm
Sat, 05 Feb 2011 20:38:32 +0100
changeset 41711 3422ae5aff3a
parent 32816 5db89f8d44f3
child 44269 3ff2fd162aee
permissions -rw-r--r--
more tracing information via Par_List.map_name;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32816
5db89f8d44f3 more official status of sequential implementations;
wenzelm
parents: 29368
diff changeset
     1
(*  Title:      Pure/Concurrent/par_list_sequential.ML
28546
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
41711
3422ae5aff3a more tracing information via Par_List.map_name;
wenzelm
parents: 32816
diff changeset
    10
fun map_name _ = map;
28546
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
85d2972fe9e6 fixed spelling;
wenzelm
parents: 28546
diff changeset
    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;