src/HOL/Finite.thy
changeset 8920 af5e09b6c208
parent 7958 f531589c9fc1
child 8962 633e1682455c