src/HOL/Finite.thy
changeset 8657 b9475dad85ed
parent 7958 f531589c9fc1
child 8962 633e1682455c