src/HOL/ex/BinEx.thy
changeset 14360 e654599b114e
parent 14124 883c38e2d4c0
child 14378 69c4d5997669