src/HOL/Finite.ML
changeset 8300 4c3f83414de3
parent 8262 08ad0a986db2
child 8320 073144bed7da