src/HOL/Numeral.thy
changeset 14722 8e739a6eaf11
parent 14443 75910c7557c5
child 14800 50581f2b2c0e