src/HOL/Code_Numeral.thy
changeset 31207 7eb05fc49b45
parent 31205 98370b26c2ce
child 31266 55e70b6d812e