src/HOL/Code_Numeral.thy
changeset 56476 dd596c2b5897
parent 55945 e96383acecf9
child 56846 9df717fef2bb