src/HOL/Code_Numeral.thy
changeset 33319 74f0dcc0b5fb
parent 33318 ddd97d9dfbfb
child 33340 a165b97f3658