src/HOL/ex/BinEx.thy
changeset 75709 a068fb7346ef
parent 63589 58aab4745e85