src/HOL/ex/BinEx.ML
changeset 9436 62bb04ab4b01
parent 9000 c20d58286a51