src/HOL/Finite.ML
changeset 5154 40fd46f3d3a1
parent 5148 74919e8f221c
child 5183 89f162de39cf