src/HOL/Finite.ML
changeset 5982 aeb97860d352
parent 5782 7559f116cb10
child 6024 cb87f103d114