src/HOL/Code_Numeral.thy
changeset 39157 b98909faaea8
parent 38857 97775f3e8722
child 39272 0b61951d2682