src/HOL/Code_Numeral.thy
changeset 67945 984c3dc46cc0
parent 67905 fe0f4eeceeb7
child 68010 3f223b9a0066