src/HOL/Library/EfficientNat.thy
changeset 22452 8a86fd2a1bf0
parent 22423 c1836b14c63a
child 22507 3572bc633d9a