| Thu, 28 May 1998 12:22:37 +0200 | wenzelm | README, Pure/ROOT.ML: version set automatically; | changeset | files |
| Thu, 28 May 1998 12:22:05 +0200 | wenzelm | version under control of Admin/makedist; | changeset | files |
| Thu, 28 May 1998 12:21:05 +0200 | wenzelm | added ml_prompts; | changeset | files |
| Thu, 28 May 1998 11:11:27 +0200 | wenzelm | added mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) | changeset | files |