src/HOL/Finite.ML
changeset 9356 30c3d3e308ee
parent 9351 5d53e3f35152
child 9399 effc8d44c89c