src/HOL/Finite.thy
changeset 7990 0a604b2fc2b1
parent 7958 f531589c9fc1
child 8962 633e1682455c