src/HOL/Code_Numeral.thy
changeset 82407 fcc0f74ac086
parent 81754 e7a77c795cf9
child 82445 bb1f2a03b370
equal deleted inserted replaced
82406:c597898ff51b 82407:fcc0f74ac086