src/HOL/Finite.ML
changeset 5526 e7617b57a3e6
parent 5516 d80e9aeb4a2b
child 5537 c2bd39a2c0ee