src/HOL/ex/BinEx.thy
changeset 58426 cac802846ff1
parent 58410 6d46ad54a2ab
child 58889 5b7a9633cfa8