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