src/HOL/Code_Numeral.thy
changeset 34120 f9920a3ddf50
parent 33340 a165b97f3658
child 34886 873c31d9f10d
child 34915 7894c7dab132