src/HOL/Finite.ML
changeset 11295 66925f23ac7f
parent 11122 0a258a048d8d
child 11451 8abfb4f7bd02