src/HOL/Finite.thy
changeset 9030 bb7622789bf2
parent 8962 633e1682455c
child 9087 12db178a78df