src/HOL/ex/BinEx.thy
changeset 14024 213dcc39358f
parent 13491 ddf6ae639f21
child 14113 7b3513ba0f86