src/HOL/Code_Numeral.thy
changeset 57354 ded92100ffd7
parent 56846 9df717fef2bb
child 57512 cc97b347b301