src/HOL/Code_Numeral.thy
changeset 45461 130c90bb80b4
parent 44821 a92f65e174cf
child 45694 4a8743618257