src/HOL/Code_Numeral.thy
changeset 59527 edaabc1ab1ed
parent 59487 adaa430fc0f7
child 59816 034b13f4efae