src/HOL/Code_Numeral.thy
changeset 82265 4b875a4c83b0
parent 81754 e7a77c795cf9
child 82445 bb1f2a03b370