src/HOL/Code_Numeral.thy
changeset 45544 c0304794e9e4
parent 44821 a92f65e174cf
child 45694 4a8743618257