src/HOL/Code_Numeral.thy
changeset 39508 dfacdb01e1ec
parent 39272 0b61951d2682
child 39818 ff9e9d5ac171