src/HOL/ex/BinEx.thy
changeset 76371 1ac2416e8432
parent 63589 58aab4745e85