src/HOL/Library/EfficientNat.thy
changeset 19785 52d71ee5c8a8
parent 19617 7cb4b67d4b97
child 19791 ab326de16ad5