src/HOL/Finite.thy
changeset 8268 722074b93cdd
parent 7958 f531589c9fc1
child 8962 633e1682455c