src/HOL/Finite.ML
changeset 4047 67b5552b1067
parent 4014 df6cd80b6387
child 4059 59c1422c9da5