src/HOL/Library/EfficientNat.thy
changeset 22270 4ccb7e6be929
parent 22046 ce84c9887e2d
child 22320 d5260836d662