src/HOL/ex/Numeral.thy
changeset 46368 ded0390eceae
parent 45703 c7a13ce60161