src/HOL/Code_Numeral.thy
changeset 70213 ff8386fc191d
parent 70017 3347396ffdb3
child 70340 7383930fc946