src/HOL/Code_Numeral.thy
changeset 71297 9f2085c499a2
parent 71195 d50a718ccf35
child 71413 65ffe9e910d4