| author | wenzelm | 
| Sat, 16 Apr 2011 20:49:48 +0200 | |
| changeset 42368 | 3b8498ac2314 | 
| parent 41711 | 3422ae5aff3a | 
| child 44269 | 3ff2fd162aee | 
| permissions | -rw-r--r-- | 
| 32816 
5db89f8d44f3
more official status of sequential implementations;
 wenzelm parents: 
29368diff
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 | 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 | 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 | 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; |