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