src/Pure/General/random_word.ML
changeset 25727 e43d91f31118
parent 25721 5ae1dc2bb5ea