src/HOL/Code_Numeral.thy
changeset 70894 15adbeb1fabd
parent 70340 7383930fc946
child 70927 cc204e10385c