src/HOL/Library/EfficientNat.thy
changeset 18396 b3e7da94b51f
parent 16900 e294033d1c0f
child 18702 7dc7dcd63224