src/HOL/Random.thy
changeset 74953 aade20a03edb
parent 74101 d804e93ae9ff
child 80175 200107cdd3ac
equal deleted inserted replaced
74952:ae2185967e67 74953:aade20a03edb