src/HOL/Finite.ML
changeset 5434 9b4bed3f394c
parent 5416 9f029e382b5d
child 5476 1c09934fe445