src/HOL/Finite.ML
changeset 3564 f886dbd91ee5
parent 3517 2547f33fa33a
child 3708 56facaebf3e3