src/HOL/Finite.ML
changeset 3362 0b268cff9344
parent 3352 04502e5431fb
child 3368 be517d000c02