src/Pure/General/random.ML
changeset 63992 3aa9837d05c7
parent 62585 5d4ed917450d