src/HOL/ex/BinEx.thy
changeset 13256 cf85c4f7dcf2
parent 13192 e961c197f141
child 13491 ddf6ae639f21