HOL-ex.Code_Binary_Nat_examples