src/HOL/Finite.ML
changeset 7584 5be4bb8e4e3f
parent 7499 23e090051cb8
child 7821 a8717f53036c