src/HOL/Random.thy
changeset 74596 55d4f8e1877f
parent 74101 d804e93ae9ff
child 80175 200107cdd3ac
equal deleted inserted replaced
74595:71bafd70acbb 74596:55d4f8e1877f