src/HOL/Code_Numeral.thy
changeset 82265 4b875a4c83b0
parent 81754 e7a77c795cf9
child 82445 bb1f2a03b370
equal deleted inserted replaced
82264:756e88885a7c 82265:4b875a4c83b0