src/HOL/Code_Numeral.thy
changeset 82364 5af097d05e99
parent 81754 e7a77c795cf9
child 82445 bb1f2a03b370