src/HOL/Finite.ML
changeset 11405 b6e3ac38397d
parent 11122 0a258a048d8d
child 11451 8abfb4f7bd02