src/Tools/random_word.ML
changeset 33649 854173fcd21c
parent 33513 b2259183e282