src/HOL/Tools/polyhash.ML
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2008-09-29 wenzelm 2008-09-29 handle _ should be avoided (spurious Interrupt will spoil the game);
2006-09-21 paulson 2006-09-21 new function hashw_int
2006-08-25 paulson 2006-08-25 using inc
2005-12-23 paulson 2005-12-23 tidied
2005-12-21 paulson 2005-12-21 new hash table module in HOL/Too/s