src/HOL/Integ/NatBin.ML
changeset 9450 c97dba47e504
parent 9425 fd6866d90ec1
child 9633 a71a83253997