src/HOL/Library/Efficient_Nat.thy
changeset 29120 8a904ff43f28
parent 28969 4ed63cdda799
child 29258 bce03c644efb