src/HOL/Library/EfficientNat.thy
changeset 15485 e93a3badc2bc
parent 15396 0a36ccb79481
child 15531 08c8dad8e399