src/Tools/cache_io.ML
2010-07-08 haftmann 2010-07-08 combinator with_tmp_dir
2010-04-07 boehmes 2010-04-07 simplified Cache_IO interface (input is just a string and not already stored in a file)
2010-03-24 boehmes 2010-03-24 use internal SHA1 digest implementation for generating hash keys
2010-03-24 boehmes 2010-03-24 remove component Cache_IO (external dependency on MD5 will be replaced by internal SHA1 digest implementation)