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