src/HOL/Library/EfficientNat.thy
changeset 17076 c7effdf2e2e2
parent 16900 e294033d1c0f
child 18702 7dc7dcd63224