src/HOL/Finite.thy
changeset 3564 f886dbd91ee5
parent 3413 c1f63cc3a768
child 5101 52e7c75acfe6