| author | haftmann | 
| Thu, 06 Nov 2008 09:09:51 +0100 | |
| changeset 28717 | 848ffc6b0b8a | 
| parent 28556 | 85d2972fe9e6 | 
| child 29368 | 503ce3f8f092 | 
| permissions | -rw-r--r-- | 
| 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 | 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; |