src/Pure/General/random.ML
changeset 79101 4e47b34fbb8e
parent 62585 5d4ed917450d