src/HOL/ex/BinEx.ML
changeset 5526 e7617b57a3e6
parent 5513 3896c7894a57
child 5545 9117a0e2bf31