src/HOL/Code_Numeral.thy
changeset 61487 f8cb97e0fd0b
parent 61275 053ec04ea866
child 61857 542f2c6da692