src/Pure/General/random.ML
changeset 77438 0030eabbe6c3
parent 62585 5d4ed917450d