src/HOL/Finite.ML
changeset 11944 0594e63e6057
parent 11786 51ce34ef5113