src/HOL/Finite.thy
changeset 3462 3472fa00b1d4
parent 3413 c1f63cc3a768
child 5101 52e7c75acfe6