src/HOL/Code_Numeral.thy
changeset 37678 0040bafffdef
parent 36176 3fe7e97ccca8
child 37947 844977c7abeb