src/HOL/Finite.ML
changeset 9803 bc883b390d91
parent 9736 332fab43628f
child 9837 7b26f2d51ba4