src/HOL/Finite.thy
changeset 4836 fc5773ae2790
parent 3413 c1f63cc3a768
child 5101 52e7c75acfe6