src/HOL/Code_Numeral.thy
changeset 39749 fa94799e3a3b
parent 39272 0b61951d2682
child 39818 ff9e9d5ac171