src/HOL/Code_Numeral.thy
changeset 70490 c42a0a0a9a8d
parent 70340 7383930fc946
child 70927 cc204e10385c