src/Pure/Concurrent/par_list_dummy.ML
author wenzelm
Wed, 31 Dec 2008 00:08:11 +0100
changeset 29264 4ea3358fac3f
parent 28556 85d2972fe9e6
child 29368 503ce3f8f092
permissions -rw-r--r--
use regular Term.add_vars, Term.add_frees etc.;
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;
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;