src/HOL/Code_Numeral.thy
changeset 82454 ba1f9fb23b8d
parent 82445 bb1f2a03b370
child 82514 efc1cd044440