src/HOL/Random.thy
changeset 58443 a23780c22245
parent 58101 e7ebe5554281
child 58889 5b7a9633cfa8
equal deleted inserted replaced
58442:039b54d9b5c4 58443:a23780c22245