src/HOL/ex/BinEx.thy
changeset 67131 85d10959c2e4
parent 63589 58aab4745e85