src/HOL/Code_Numeral.thy
changeset 57987 ecb227b40907
parent 57512 cc97b347b301
child 58306 117ba6cbe414