src/HOL/Code_Numeral.thy
changeset 39301 e1bd8a54c40f
parent 39272 0b61951d2682
child 39818 ff9e9d5ac171