src/HOL/Code_Numeral.thy
changeset 82314 c95eca07f6a0
parent 81754 e7a77c795cf9
child 82445 bb1f2a03b370