src/HOL/Library/EfficientNat.thy
changeset 22567 1565d476a9e2
parent 22507 3572bc633d9a
child 22743 e2b06bfe471a