src/HOL/ex/BinEx.thy
changeset 12542 ff5e3f11e1ef
parent 11868 56db9f3a6b3e
child 12613 279facb4253a