src/HOL/Finite.thy
changeset 4628 0c7e97836e3c
parent 3413 c1f63cc3a768
child 5101 52e7c75acfe6