src/HOL/ex/BinEx.thy
changeset 7141 a67dde8820c0
parent 6920 c912740c3545
child 9297 bafe45732b10