src/HOL/Import/HOL/word_num.imp
changeset 20907 9673c67dde9b
parent 14516 a183dec876ab