src/HOL/Finite.ML
changeset 10434 6ea4735c3955
parent 10375 d943898cc3a9
child 10785 53547a02f2a1