src/HOL/Code_Numeral.thy
changeset 59810 e749a0f2f401
parent 59487 adaa430fc0f7
child 59816 034b13f4efae