src/HOL/ex/BinEx.thy
changeset 12459 6978ab7cac64
parent 11868 56db9f3a6b3e
child 12613 279facb4253a