src/HOL/Code_Numeral.thy
changeset 59582 0fbed69ff081
parent 59487 adaa430fc0f7
child 59816 034b13f4efae