src/Tools/cache_io.ML
Thu, 08 Jul 2010 09:36:23 +0200 combinator with_tmp_dir
Wed, 07 Apr 2010 20:40:42 +0200 simplified Cache_IO interface (input is just a string and not already stored in a file)
Wed, 24 Mar 2010 09:43:34 +0100 use internal SHA1 digest implementation for generating hash keys
Wed, 24 Mar 2010 08:22:43 +0100 remove component Cache_IO (external dependency on MD5 will be replaced by internal SHA1 digest implementation)