src/HOL/Library/EfficientNat.thy
changeset 22910 54d231cbc19a
parent 22900 f8a7c10e1bd0
child 22921 475ff421a6a3